Global Index

other

(2142 entries)

Notation Index

other

(161 entries)

Module Index

other

(71 entries)

Variable Index

other

(7 entries)

Library Index

other

(24 entries)

Lemma Index

other

(496 entries)

Axiom Index

other

(11 entries)

Constructor Index

other

(749 entries)

Inductive Index

other

(140 entries)

Section Index

other

(3 entries)

Abbreviation Index

other

(55 entries)

Definition Index

other

(425 entries)

Global Index

A

abs [constructor, in Norm]
abs [constructor, in Sub]
abs [constructor, in RecordSub]
abs_arrow [lemma, in Sub]
abs_arrow [lemma, in RecordSub]
aequiv [definition, in Equiv]
aequiv_example [lemma, in Equiv]
aeval [definition, in Imp]
_ \\ _ (type_scope) [notation, in Imp]
aevalR_extended.E_AMult [constructor, in Imp]
aevalR_extended.E_AMinus [constructor, in Imp]
aevalR_extended.E_APlus [constructor, in Imp]
aevalR_extended.E_ANum [constructor, in Imp]
aevalR_extended.E_Any [constructor, in Imp]
aevalR_extended.aevalR [inductive, in Imp]
aevalR_extended.AMult [constructor, in Imp]
aevalR_extended.AMinus [constructor, in Imp]
aevalR_extended.APlus [constructor, in Imp]
aevalR_extended.ANum [constructor, in Imp]
aevalR_extended.AAny [constructor, in Imp]
aevalR_extended.aexp [inductive, in Imp]
aevalR_extended [module, in Imp]
_ \\ _ (type_scope) [notation, in Imp]
aevalR_division.E_ADiv [constructor, in Imp]
aevalR_division.E_AMult [constructor, in Imp]
aevalR_division.E_AMinus [constructor, in Imp]
aevalR_division.E_APlus [constructor, in Imp]
aevalR_division.E_ANum [constructor, in Imp]
aevalR_division.aevalR [inductive, in Imp]
aevalR_division.ADiv [constructor, in Imp]
aevalR_division.AMult [constructor, in Imp]
aevalR_division.AMinus [constructor, in Imp]
aevalR_division.APlus [constructor, in Imp]
aevalR_division.ANum [constructor, in Imp]
aevalR_division.aexp [inductive, in Imp]
aevalR_division [module, in Imp]
aeval_weakening [lemma, in Equiv]
aexp [inductive, in Imp]
AExp [module, in Imp]
AExp.aeval [definition, in Imp]
AExp.aevalR [inductive, in Imp]
_ \\ _ (type_scope) [notation, in Imp]
AExp.aevalR_first_try.TooHardToRead.E_AMult [constructor, in Imp]
AExp.aevalR_first_try.TooHardToRead.E_AMinus [constructor, in Imp]
AExp.aevalR_first_try.TooHardToRead.E_APlus [constructor, in Imp]
AExp.aevalR_first_try.TooHardToRead.E_ANum [constructor, in Imp]
AExp.aevalR_first_try.TooHardToRead.aevalR [inductive, in Imp]
AExp.aevalR_first_try.TooHardToRead [module, in Imp]
AExp.aevalR_first_try.E_AMult [constructor, in Imp]
AExp.aevalR_first_try.E_AMinus [constructor, in Imp]
AExp.aevalR_first_try.E_APlus [constructor, in Imp]
AExp.aevalR_first_try.E_ANum [constructor, in Imp]
AExp.aevalR_first_try.aevalR [inductive, in Imp]
AExp.aevalR_first_try [module, in Imp]
AExp.aeval_iff_aevalR' [lemma, in Imp]
AExp.aeval_iff_aevalR [lemma, in Imp]
AExp.aexp [inductive, in Imp]
AExp.AMinus [constructor, in Imp]
AExp.AMult [constructor, in Imp]
AExp.ANum [constructor, in Imp]
AExp.APlus [constructor, in Imp]
AExp.BAnd [constructor, in Imp]
AExp.BEq [constructor, in Imp]
AExp.beval [definition, in Imp]
AExp.bevalR [inductive, in Imp]
AExp.beval_iff_bevalR [lemma, in Imp]
AExp.bexp [inductive, in Imp]
AExp.BFalse [constructor, in Imp]
AExp.BLe [constructor, in Imp]
AExp.BNot [constructor, in Imp]
AExp.BTrue [constructor, in Imp]
AExp.E_AMult [constructor, in Imp]
AExp.E_AMinus [constructor, in Imp]
AExp.E_APlus [constructor, in Imp]
AExp.E_ANum [constructor, in Imp]
AExp.foo [lemma, in Imp]
AExp.foo' [lemma, in Imp]
AExp.In10 [lemma, in Imp]
AExp.In10' [lemma, in Imp]
AExp.manual_grade_for_beval_rules [definition, in Imp]
AExp.optimize_0plus_b_sound [lemma, in Imp]
AExp.optimize_0plus_b [definition, in Imp]
AExp.optimize_0plus_sound'' [lemma, in Imp]
AExp.optimize_0plus_sound' [lemma, in Imp]
AExp.optimize_0plus_sound [lemma, in Imp]
AExp.optimize_0plus [definition, in Imp]
AExp.silly_presburger_example [definition, in Imp]
AExp.silly1 [lemma, in Imp]
AExp.silly2 [lemma, in Imp]
AExp.test_optimize_0plus [definition, in Imp]
AExp.test_aeval1 [definition, in Imp]
_ \\ _ (type_scope) [notation, in Imp]
aexp1 [definition, in Imp]
afi_test2 [constructor, in Norm]
afi_test1 [constructor, in Norm]
afi_test0 [constructor, in Norm]
afi_snd [constructor, in Norm]
afi_fst [constructor, in Norm]
afi_pair2 [constructor, in Norm]
afi_pair1 [constructor, in Norm]
afi_abs [constructor, in Norm]
afi_app2 [constructor, in Norm]
afi_app1 [constructor, in Norm]
afi_var [constructor, in Norm]
afi_test3 [constructor, in Sub]
afi_test2 [constructor, in Sub]
afi_test1 [constructor, in Sub]
afi_abs [constructor, in Sub]
afi_app2 [constructor, in Sub]
afi_app1 [constructor, in Sub]
afi_var [constructor, in Sub]
afi_rtail [constructor, in RecordSub]
afi_rhead [constructor, in RecordSub]
afi_proj [constructor, in RecordSub]
afi_abs [constructor, in RecordSub]
afi_app2 [constructor, in RecordSub]
afi_app1 [constructor, in RecordSub]
afi_var [constructor, in RecordSub]
AId [constructor, in Imp]
always_loop_hoare [lemma, in Hoare]
AMinus [constructor, in Imp]
AMult [constructor, in Imp]
ANum [constructor, in Imp]
APlus [constructor, in Imp]
app [constructor, in Norm]
app [constructor, in Sub]
app [constructor, in RecordSub]
appears_free_in [inductive, in Norm]
appears_free_in [inductive, in Sub]
appears_free_in [inductive, in RecordSub]
apply_empty [lemma, in Maps]
Arrow [constructor, in Norm]
Arrow [constructor, in Sub]
Arrow [constructor, in RecordSub]
Assertion [definition, in Hoare]
assert_implies [definition, in Hoare]
Assign [constructor, in PE]
assign [definition, in PE]
assigned [definition, in PE]
assign_aequiv [lemma, in Equiv]
assign_removes [lemma, in PE]
assn_sub_example2 [definition, in Hoare]
assn_sub_example [definition, in Hoare]
assn_sub [definition, in Hoare]
astep [inductive, in Smallstep]
AS_Mult [constructor, in Smallstep]
AS_Mult2 [constructor, in Smallstep]
AS_Mult1 [constructor, in Smallstep]
AS_Minus [constructor, in Smallstep]
AS_Minus2 [constructor, in Smallstep]
AS_Minus1 [constructor, in Smallstep]
AS_Plus [constructor, in Smallstep]
AS_Plus2 [constructor, in Smallstep]
AS_Plus1 [constructor, in Smallstep]
AS_Id [constructor, in Smallstep]
atrans_sound [definition, in Equiv]
aval [inductive, in Smallstep]
av_num [constructor, in Smallstep]

B

BAnd [constructor, in Imp]
Base [constructor, in Sub]
Base [constructor, in RecordSub]
bassn [definition, in Hoare]
bassn_eval_false [lemma, in HoareAsLogic]
BEq [constructor, in Imp]
bequiv [definition, in Equiv]
bequiv_example [lemma, in Equiv]
beval [definition, in Imp]
bexp [inductive, in Imp]
bexp_eval_false [lemma, in Hoare]
bexp_eval_true [lemma, in Hoare]
bexp1 [definition, in Imp]
BFalse [constructor, in Imp]
Bib [library]
BLe [constructor, in Imp]
block [inductive, in PE]
BNot [constructor, in Imp]
body [constructor, in PE]
Bool [constructor, in Norm]
Bool [constructor, in Sub]
Bool [constructor, in Types]
bool_to_bexp [definition, in Imp]
bool_canonical [lemma, in Types]
boxer [constructor, in LibTactics]
Boxer [inductive, in LibTactics]
BreakImp [module, in Imp]
BreakImp.break_ignore [lemma, in Imp]
BreakImp.CAss [constructor, in Imp]
BreakImp.CBreak [constructor, in Imp]
BreakImp.ceval [inductive, in Imp]
BreakImp.ceval_deterministic [lemma, in Imp]
BreakImp.CIf [constructor, in Imp]
BreakImp.com [inductive, in Imp]
BreakImp.CSeq [constructor, in Imp]
BreakImp.CSkip [constructor, in Imp]
BreakImp.CWhile [constructor, in Imp]
BreakImp.E_Skip [constructor, in Imp]
BreakImp.result [inductive, in Imp]
BreakImp.SBreak [constructor, in Imp]
BreakImp.SContinue [constructor, in Imp]
BreakImp.while_break_true [lemma, in Imp]
BreakImp.while_stops_on_break [lemma, in Imp]
BreakImp.while_continue [lemma, in Imp]
_ =[ _ ]=> _ / _ [notation, in Imp]
_ ;; _ [notation, in Imp]
_ ::= _ [notation, in Imp]
BREAK [notation, in Imp]
SKIP [notation, in Imp]
TEST _ THEN _ ELSE _ FI [notation, in Imp]
WHILE _ DO _ END [notation, in Imp]
bstep [inductive, in Smallstep]
BS_AndFalse [constructor, in Smallstep]
BS_AndTrueFalse [constructor, in Smallstep]
BS_AndTrueTrue [constructor, in Smallstep]
BS_AndStep [constructor, in Smallstep]
BS_AndTrueStep [constructor, in Smallstep]
BS_NotFalse [constructor, in Smallstep]
BS_NotTrue [constructor, in Smallstep]
BS_NotStep [constructor, in Smallstep]
BS_LtEq [constructor, in Smallstep]
BS_LtEq2 [constructor, in Smallstep]
BS_LtEq1 [constructor, in Smallstep]
BS_Eq [constructor, in Smallstep]
BS_Eq2 [constructor, in Smallstep]
BS_Eq1 [constructor, in Smallstep]
btrans_sound [definition, in Equiv]
BTrue [constructor, in Imp]
bvalue [inductive, in Types]
bv_fls [constructor, in Types]
bv_tru [constructor, in Types]

C

D

E

F

fact_in_coq [definition, in Imp]
False_and_P_imp [lemma, in HoareAsLogic]
false_eqb_string [lemma, in Maps]
fib [definition, in Hoare2]
fib_eqn [lemma, in Hoare2]
find_parity_correct' [lemma, in Hoare2]
find_parity_dec' [definition, in Hoare2]
find_parity_correct [lemma, in Hoare2]
find_parity_dec [definition, in Hoare2]
find_parity [definition, in Hoare2]
FirstTry [module, in Typechecking]
FirstTry.type_check [definition, in Typechecking]
fls [constructor, in Norm]
fls [constructor, in Sub]
fls [constructor, in Types]
fold_constants_com_sound [lemma, in Equiv]
fold_constants_bexp_sound [lemma, in Equiv]
fold_constants_aexp_sound [lemma, in Equiv]
fold_com_ex1 [definition, in Equiv]
fold_constants_com [definition, in Equiv]
fold_bexp_ex2 [definition, in Equiv]
fold_bexp_ex1 [definition, in Equiv]
fold_constants_bexp [definition, in Equiv]
fold_aexp_ex2 [definition, in Equiv]
fold_aexp_ex1 [definition, in Equiv]
fold_constants_aexp [definition, in Equiv]
free_in_context [lemma, in Norm]
free_in_context [lemma, in Sub]
free_in_context [lemma, in RecordSub]
fst [constructor, in Norm]

G

GenExample [module, in UseTactics]
GenExample.substitution_preserves_typing [lemma, in UseTactics]
Goto [constructor, in PE]
gt_not_le [axiom, in UseAuto]

H

I

K

keval [definition, in PE]
keval_example [definition, in PE]

L

M

manual_grade_for_combined_properties [definition, in Smallstep]
manual_grade_for_eval__multistep_inf [definition, in Smallstep]
manual_grade_for_equiv_classes [definition, in Equiv]
manual_grade_for_no_whiles_terminating [definition, in Imp]
manual_grade_for_XtimesYinZ_spec [definition, in Imp]
manual_grade_for_norm [definition, in Norm]
manual_grade_for_norm_fail [definition, in Norm]
manual_grade_for_products [definition, in Sub]
manual_grade_for_variations [definition, in Sub]
manual_grade_for_pair_permutation [definition, in Sub]
manual_grade_for_smallest_2 [definition, in Sub]
manual_grade_for_smallest_1 [definition, in Sub]
manual_grade_for_small_large_4 [definition, in Sub]
manual_grade_for_small_large_2 [definition, in Sub]
manual_grade_for_small_large_1 [definition, in Sub]
manual_grade_for_proper_subtypes [definition, in Sub]
manual_grade_for_subtype_concepts_tf [definition, in Sub]
manual_grade_for_subtype_instances_tf_2 [definition, in Sub]
manual_grade_for_subtype_order [definition, in Sub]
manual_grade_for_arrow_sub_wrong [definition, in Sub]
manual_grade_for_hoare_repeat [definition, in Hoare]
manual_grade_for_if1_hoare [definition, in Hoare]
manual_grade_for_hoarestate1 [definition, in Hoare]
manual_grade_for_hoare_asgn_examples_2 [definition, in Hoare]
manual_grade_for_hoare_asgn_wrong [definition, in Hoare]
manual_grade_for_hoare_asgn_examples [definition, in Hoare]
manual_grade_for_rcd_types_match_informal [definition, in RecordSub]
manual_grade_for_factorial_dec [definition, in Hoare2]
manual_grade_for_check_defn_of_slow_assignment_dec [definition, in Hoare2]
manual_grade_for_decorations_in_two_loops [definition, in Hoare2]
manual_grade_for_decorations_in_Min_Hoare [definition, in Hoare2]
manual_grade_for_decorations_in_factorial [definition, in Hoare2]
manual_grade_for_decorations_in_slow_assignment [definition, in Hoare2]
manual_grade_for_decorations_in_if_minus_plus_reloaded [definition, in Hoare2]
manual_grade_for_prog_pres_bigstep [definition, in Types]
manual_grade_for_remove_predzro [definition, in Types]
manual_grade_for_variation2 [definition, in Types]
manual_grade_for_variation1 [definition, in Types]
manual_grade_for_subject_expansion [definition, in Types]
manual_grade_for_finish_preservation_informal [definition, in Types]
manual_grade_for_finish_progress_informal [definition, in Types]
Maps [library]
MoreStlc [library]
msubst [definition, in Norm]
msubst_R [lemma, in Norm]
msubst_preserves_typing [lemma, in Norm]
msubst_app [lemma, in Norm]
msubst_abs [lemma, in Norm]
msubst_var [lemma, in Norm]
msubst_closed [lemma, in Norm]
multi [inductive, in Smallstep]
multistep [abbreviation, in Norm]
multistep [definition, in Types]
multistep__eval [lemma, in Smallstep]
multistep_congr_2 [lemma, in Smallstep]
multistep_congr_1 [lemma, in Smallstep]
multistep_App2 [lemma, in Norm]
multistep_preserves_R' [lemma, in Norm]
multistep_preserves_R [lemma, in Norm]
multi_trans [lemma, in Smallstep]
multi_R [lemma, in Smallstep]
multi_step [constructor, in Smallstep]
multi_refl [constructor, in Smallstep]
mupdate [definition, in Norm]
mupdate_drop [lemma, in Norm]
mupdate_lookup [lemma, in Norm]
myFact [definition, in UseAuto]

N

NaryExamples [module, in UseTactics]
NaryExamples.demo_branch [lemma, in UseTactics]
NaryExamples.demo_splits [lemma, in UseTactics]
Nat [constructor, in Types]
nat_le_refl [lemma, in UseAuto]
nat_canonical [lemma, in Types]
negation_study_2 [lemma, in UseAuto]
negation_study_1 [lemma, in UseAuto]
nf_same_as_value [lemma, in Smallstep]
nf_is_value [lemma, in Smallstep]
Norm [library]
normalization [lemma, in Norm]
normalize_ex' [lemma, in Smallstep]
normalize_ex [lemma, in Smallstep]
normalizing [definition, in Smallstep]
normal_forms_unique [lemma, in Smallstep]
normal_form_of [definition, in Smallstep]
normal_form [definition, in Smallstep]
no_whiles_eqv [lemma, in Imp]
no_whilesR [inductive, in Imp]
no_whiles [definition, in Imp]
nvalue [inductive, in Types]
nv_scc [constructor, in Types]
nv_zro [constructor, in Types]

O

omega_demo_4 [lemma, in UseAuto]
omega_demo_3 [lemma, in UseAuto]
omega_demo_2 [lemma, in UseAuto]
omega_demo_1 [lemma, in UseAuto]
order_matters_2 [lemma, in UseAuto]
order_matters_1 [lemma, in UseAuto]

P

P [constructor, in Smallstep]
P [axiom, in UseAuto]
pair [constructor, in Norm]
parity [definition, in PE]
parity [definition, in Hoare2]
parity_eval [definition, in PE]
parity_body [definition, in PE]
parity_label [inductive, in PE]
parity_dec_correct [lemma, in Hoare2]
parity_dec [definition, in Hoare2]
parity_correct [lemma, in Hoare2]
parity_lt_2 [lemma, in Hoare2]
parity_ge_2 [lemma, in Hoare2]
partial_map [definition, in Maps]
PE [library]
peval [inductive, in PE]
pe_program_correct [lemma, in PE]
pe_peval_intro [constructor, in PE]
pe_peval [inductive, in PE]
pe_program [definition, in PE]
pe_block_correct [lemma, in PE]
pe_block_example [definition, in PE]
pe_block [definition, in PE]
pe_com_correct [lemma, in PE]
pe_com_sound [lemma, in PE]
pe_com_complete [lemma, in PE]
pe_ceval_intro [constructor, in PE]
pe_ceval [inductive, in PE]
pe_example3 [definition, in PE]
pe_example2 [definition, in PE]
pe_example1 [definition, in PE]
PE_If [constructor, in PE]
PE_IfFalse [constructor, in PE]
PE_IfTrue [constructor, in PE]
PE_Seq [constructor, in PE]
PE_AssDynamic [constructor, in PE]
PE_AssStatic [constructor, in PE]
PE_Skip [constructor, in PE]
pe_com [inductive, in PE]
pe_compare_update [lemma, in PE]
pe_compare_removes [lemma, in PE]
pe_removes_correct [lemma, in PE]
pe_removes [definition, in PE]
pe_compare_correct [lemma, in PE]
pe_compare [definition, in PE]
pe_unique_correct [lemma, in PE]
pe_unique [definition, in PE]
pe_disagree_domain [lemma, in PE]
pe_disagree_at [definition, in PE]
pe_update_update_add [lemma, in PE]
pe_update_update_remove [lemma, in PE]
pe_add_correct [lemma, in PE]
pe_add [definition, in PE]
pe_remove_correct [lemma, in PE]
pe_remove [definition, in PE]
pe_bexp_correct [lemma, in PE]
pe_bexp [definition, in PE]
pe_aexp_correct [lemma, in PE]
pe_consistent_update [lemma, in PE]
pe_update_consistent [lemma, in PE]
pe_update_correct [lemma, in PE]
pe_update [definition, in PE]
pe_aexp_correct_weak [lemma, in PE]
pe_consistent [definition, in PE]
pe_aexp [definition, in PE]
pe_domain [lemma, in PE]
pe_lookup [definition, in PE]
pe_state [definition, in PE]
plus2 [definition, in Imp]
plus2_spec [lemma, in Imp]
post [definition, in Hoare2]
Postscript [library]
post_dec [definition, in Hoare2]
pow2 [definition, in Hoare2]
pow2_le_1 [lemma, in Hoare2]
pow2_plus_1 [lemma, in Hoare2]
prd [constructor, in Types]
Preface [library]
preservation [lemma, in Norm]
preservation [lemma, in Sub]
preservation [lemma, in RecordSub]
preservation [lemma, in Types]
PreservationProgressReferences [module, in UseAuto]
PreservationProgressReferences.nth_eq_last' [lemma, in UseAuto]
PreservationProgressReferences.preservation [lemma, in UseAuto]
PreservationProgressReferences.preservation_ref [lemma, in UseAuto]
PreservationProgressReferences.preservation' [lemma, in UseAuto]
PreservationProgressReferences.progress [lemma, in UseAuto]
PreservationProgressStlc [module, in UseAuto]
PreservationProgressStlc.preservation [lemma, in UseAuto]
PreservationProgressStlc.preservation' [lemma, in UseAuto]
PreservationProgressStlc.progress [lemma, in UseAuto]
PreservationProgressStlc.progress' [lemma, in UseAuto]
preservation' [lemma, in Types]
pre_dec [definition, in Hoare2]
Prod [constructor, in Norm]
prog [definition, in Smallstep]
program [definition, in PE]
progress [lemma, in Sub]
progress [lemma, in RecordSub]
progress [lemma, in Types]
prog_i [definition, in Equiv]
prog_h [definition, in Equiv]
prog_g [definition, in Equiv]
prog_f [definition, in Equiv]
prog_e [definition, in Equiv]
prog_d [definition, in Equiv]
prog_c [definition, in Equiv]
prog_b [definition, in Equiv]
prog_a [definition, in Equiv]
pup_to_2_ceval [lemma, in Imp]
pup_to_n [definition, in Imp]

R

S

T

U

UnfoldsExample [module, in UseTactics]
UnfoldsExample.bexp_eval_true [lemma, in UseTactics]
unit [constructor, in Sub]
Unit [constructor, in Sub]
update [definition, in Maps]
update_permute [lemma, in Maps]
update_same [lemma, in Maps]
update_shadow [lemma, in Maps]
update_neq [lemma, in Maps]
update_eq [lemma, in Maps]
update_example4 [definition, in Maps]
update_example3 [definition, in Maps]
update_example2 [definition, in Maps]
update_example1 [definition, in Maps]
UseAuto [library]
UseTactics [library]

V

vacuous_substitution [lemma, in Norm]
value [inductive, in Smallstep]
value [inductive, in Norm]
value [inductive, in Sub]
value [inductive, in RecordSub]
value [definition, in Types]
value_is_nf [lemma, in Smallstep]
value_halts [lemma, in Norm]
value__normal [lemma, in Norm]
value_is_nf [lemma, in Types]
var [constructor, in Norm]
var [constructor, in Sub]
var [constructor, in RecordSub]
var_not_used_in_aexp [inductive, in Equiv]
verification_correct_dec [lemma, in Hoare2]
verification_conditions_dec [definition, in Hoare2]
verification_correct [lemma, in Hoare2]
verification_conditions [definition, in Hoare2]
VNUId [constructor, in Equiv]
VNUMinus [constructor, in Equiv]
VNUMult [constructor, in Equiv]
VNUNum [constructor, in Equiv]
VNUPlus [constructor, in Equiv]
v_const [constructor, in Smallstep]
V_cons [constructor, in Norm]
V_nil [constructor, in Norm]
v_fls [constructor, in Norm]
v_tru [constructor, in Norm]
v_pair [constructor, in Norm]
v_abs [constructor, in Norm]
v_unit [constructor, in Sub]
v_false [constructor, in Sub]
v_true [constructor, in Sub]
v_abs [constructor, in Sub]
v_rcons [constructor, in RecordSub]
v_rnil [constructor, in RecordSub]
v_abs [constructor, in RecordSub]

W

W [definition, in Imp]
well_formed_ty [inductive, in RecordSub]
wfArrow [constructor, in RecordSub]
wfBase [constructor, in RecordSub]
wfRCons [constructor, in RecordSub]
wfRNil [constructor, in RecordSub]
wfTop [constructor, in RecordSub]
wf_rcd_lookup [lemma, in RecordSub]
WHILE_true [lemma, in Equiv]
WHILE_true_nonterm [lemma, in Equiv]
WHILE_false [lemma, in Equiv]
while_example [definition, in Hoare]
working_of_auto_2 [lemma, in UseAuto]
working_of_auto_1 [lemma, in UseAuto]
wp [definition, in HoareAsLogic]
wp_is_weakest [lemma, in HoareAsLogic]
wp_is_precondition [lemma, in HoareAsLogic]

X

X [definition, in Imp]
XtimesYinZ [definition, in Imp]

Y

Y [definition, in Imp]

Z

Z [definition, in Imp]
zprop [definition, in Equiv]
zprop_preserving [lemma, in Equiv]
zro [constructor, in Types]

other

Notation Index

A

_ \\ _ (type_scope) [in Imp]
_ \\ _ (type_scope) [in Imp]
_ \\ _ (type_scope) [in Imp]
_ \\ _ (type_scope) [in Imp]

B

_ =[ _ ]=> _ / _ [in Imp]
_ ;; _ [in Imp]
_ ::= _ [in Imp]
BREAK [in Imp]
SKIP [in Imp]
TEST _ THEN _ ELSE _ FI [in Imp]
WHILE _ DO _ END [in Imp]

C

_ / _ -->* _ / _ [in Smallstep]
_ / _ --> _ / _ [in Smallstep]
_ ;; _ [in Smallstep]
_ ::= _ [in Smallstep]
PAR _ WITH _ END [in Smallstep]
SKIP [in Smallstep]
TEST _ THEN _ ELSE _ FI [in Smallstep]
WHILE _ DO _ END [in Smallstep]
_ --> _ [in Smallstep]

H

{{ _ }} _ {{ _ }} (hoare_spec_scope) [in Hoare]
HAVOC _ (imp_scope) [in Equiv]
TEST _ THEN _ ELSE _ FI (imp_scope) [in Equiv]
WHILE _ DO _ END (imp_scope) [in Equiv]
_ ;; _ (imp_scope) [in Equiv]
_ ::= _ (imp_scope) [in Equiv]
SKIP (imp_scope) [in Equiv]
_ =[ _ ]=> _ [in Equiv]
_ =[ _ ]=> _ [in Hoare]
_ ;; _ [in Hoare]
_ ::= _ [in Hoare]
HAVOC _ [in Hoare]
SKIP [in Hoare]
TEST _ THEN _ ELSE _ FI [in Hoare]
WHILE _ DO _ END [in Hoare]
{{ _ }} _ {{ _ }} (hoare_spec_scope) [in Hoare]
_ =[ _ ]=> _ [in Hoare]
_ ;; _ [in Hoare]
_ ::= _ [in Hoare]
ASSERT _ [in Hoare]
ASSUME _ [in Hoare]
SKIP [in Hoare]
TEST _ THEN _ ELSE _ FI [in Hoare]
WHILE _ DO _ END [in Hoare]

I

{{ _ }} _ {{ _ }} (hoare_spec_scope) [in Hoare]
IF1 _ THEN _ FI (imp_scope) [in Hoare]
TEST _ THEN _ ELSE _ FI (imp_scope) [in Hoare]
WHILE _ DO _ END (imp_scope) [in Hoare]
_ ::= _ (imp_scope) [in Hoare]
_ ;; _ (imp_scope) [in Hoare]
SKIP (imp_scope) [in Hoare]
_ =[ _ ]=> _ [in Hoare]

L

_ / _ / _ / _ \\ _ # _ [in PE]
_ / _ \\ _ # _ [in PE]
_ / _ \\ _ / _ / _ [in PE]

R

_ =[ _ ]=> _ [in Hoare]
_ ::= _ [in Hoare]
_ ;; _ [in Hoare]
REPEAT _ UNTIL _ END [in Hoare]
SKIP [in Hoare]
TEST _ THEN _ ELSE _ FI [in Hoare]
WHILE _ DO _ END [in Hoare]
{{ _ }} _ {{ _ }} [in Hoare]

S

_ --> _ [in Smallstep]
_ |- _ \in _ [in Records]
_ -->* _ [in Records]
_ --> _ [in Records]
[ _ := _ ] _ [in Records]
_ |- _ \in _ [in MoreStlc]
_ -->* _ [in MoreStlc]
_ --> _ [in MoreStlc]
[ _ := _ ] _ [in MoreStlc]
_ / _ -->+ _ / _ [in References]
_ ; _ |- _ \in _ [in References]
_ / _ -->* _ / _ [in References]
_ / _ --> _ / _ [in References]
[ _ := _ ] _ [in References]
_ |- _ \in _ [in Stlc]
_ -->* _ [in Stlc]
_ --> _ [in Stlc]
[ _ := _ ] _ [in Stlc]

T

_ --> _ [in Smallstep]
_ --> _ [in Smallstep]
_ --> _ [in Smallstep]
_ --> _ [in Smallstep]
_ --> _ [in Smallstep]

other

Module Index

A

aevalR_extended [in Imp]
aevalR_division [in Imp]
AExp [in Imp]
AExp.aevalR_first_try.TooHardToRead [in Imp]
AExp.aevalR_first_try [in Imp]

B

BreakImp [in Imp]

C

CImp [in Smallstep]
Combined [in Smallstep]

D

DeterministicImp [in UseAuto]

E

EqualityExamples [in UseTactics]
Examples [in Sub]
Examples [in RecordSub]
ExamplesInstantiations [in UseTactics]
ExamplesLets [in UseTactics]
Examples2 [in Sub]
Examples2 [in RecordSub]
ExAssertions [in Hoare]

F

FirstTry [in Typechecking]

G

GenExample [in UseTactics]

H

Himp [in Equiv]
Himp [in Hoare]
Himp2 [in Hoare2]
HoareAssertAssume [in Hoare]

I

If1 [in Hoare]
IntrovExamples [in UseTactics]
InvertsExamples [in UseTactics]

L

LibTacticsCompatibility [in LibTactics]
Loop [in PE]

N

NaryExamples [in UseTactics]

P

PreservationProgressReferences [in UseAuto]
PreservationProgressStlc [in UseAuto]

R

RepeatExercise [in Hoare]
RingDemo [in UseAuto]

S

T

Temp1 [in Smallstep]
Temp2 [in Smallstep]
Temp3 [in Smallstep]
Temp4 [in Smallstep]
Temp4.Temp5 [in Smallstep]
TypecheckerExtensions [in Typechecking]

U

UnfoldsExample [in UseTactics]

Variable Index

E

equatesLemma.A0 [in LibTactics]
equatesLemma.A1 [in LibTactics]
equatesLemma.A2 [in LibTactics]
equatesLemma.A3 [in LibTactics]
equatesLemma.A4 [in LibTactics]
equatesLemma.A5 [in LibTactics]
equatesLemma.A6 [in LibTactics]

Library Index

B

Bib

E

Equiv

H

Hoare
HoareAsLogic
Hoare2

I

Imp

L

LibTactics

M

Maps
MoreStlc

N

Norm

P

PE
Postscript
Preface

R

Records
RecordSub
References

S

Smallstep
Stlc
StlcProp
Sub

T

Typechecking
Types

U

UseAuto
UseTactics

Lemma Index

A

abs_arrow [in Sub]
abs_arrow [in RecordSub]
aequiv_example [in Equiv]
aeval_weakening [in Equiv]
AExp.aeval_iff_aevalR' [in Imp]
AExp.aeval_iff_aevalR [in Imp]
AExp.beval_iff_bevalR [in Imp]
AExp.foo [in Imp]
AExp.foo' [in Imp]
AExp.In10 [in Imp]
AExp.In10' [in Imp]
AExp.optimize_0plus_b_sound [in Imp]
AExp.optimize_0plus_sound'' [in Imp]
AExp.optimize_0plus_sound' [in Imp]
AExp.optimize_0plus_sound [in Imp]
AExp.silly1 [in Imp]
AExp.silly2 [in Imp]
always_loop_hoare [in Hoare]
apply_empty [in Maps]
assign_aequiv [in Equiv]
assign_removes [in PE]

B

bassn_eval_false [in HoareAsLogic]
bequiv_example [in Equiv]
bexp_eval_false [in Hoare]
bexp_eval_true [in Hoare]
bool_canonical [in Types]
BreakImp.break_ignore [in Imp]
BreakImp.ceval_deterministic [in Imp]
BreakImp.while_break_true [in Imp]
BreakImp.while_stops_on_break [in Imp]
BreakImp.while_continue [in Imp]

C

canonical_forms_of_Bool [in Sub]
canonical_forms_of_arrow_types [in Sub]
canonical_forms_of_arrow_types [in RecordSub]
CAss_congruence [in Equiv]
ceval_deterministic [in Imp]
ceval_extensionality [in PE]
CIf_congruence [in Equiv]
CImp.par_loop_any_X [in Smallstep]
CImp.par_body_n [in Smallstep]
CImp.par_body_n__Sn [in Smallstep]
cmin_minimal [in Equiv]
compiler_is_correct [in Smallstep]
congruence_demo_3 [in UseAuto]
congruence_demo_4 [in UseAuto]
congruence_demo_2 [in UseAuto]
congruence_demo_1 [in UseAuto]
context_invariance [in Norm]
context_invariance [in Sub]
context_invariance [in RecordSub]
CSeq_congruence [in Equiv]
CWhile_congruence [in Equiv]
c3_c4_different [in Equiv]

D

dec_while_correct [in Hoare2]
demo_tryfalse [in UseTactics]
demo_false_arg [in UseTactics]
demo_false [in UseTactics]
demo_false [in UseAuto]
demo_auto_absurd_2 [in UseAuto]
demo_auto_absurd_1 [in UseAuto]
demo_hint_unfold_context_2 [in UseAuto]
demo_hint_unfold_context_1 [in UseAuto]
demo_hint_unfold_goal_2 [in UseAuto]
demo_hint_unfold_goal_1 [in UseAuto]
demo_clears_all_and_clears_but [in LibTactics]
DeterministicImp.ceval_deterministic'''' [in UseAuto]
DeterministicImp.ceval_deterministic''' [in UseAuto]
DeterministicImp.ceval_deterministic'' [in UseAuto]
DeterministicImp.ceval_deterministic' [in UseAuto]
DeterministicImp.ceval_deterministic [in UseAuto]
dfib_correct [in Hoare2]
div_mod_dec_correct [in Hoare2]
dpow2_down_correct [in Hoare2]
duplicate_subst [in Norm]
dup_lemma [in LibTactics]

E

eqb_stringP [in Maps]
eqb_string_false_iff [in Maps]
eqb_string_true_iff [in Maps]
eqb_string_refl [in Maps]
EqualityExamples.demo_applys_eq_3 [in UseTactics]
EqualityExamples.demo_applys_eq_2 [in UseTactics]
EqualityExamples.demo_applys_eq_1 [in UseTactics]
EqualityExamples.demo_fequals [in UseTactics]
EqualityExamples.demo_substs [in UseTactics]
EqualityExamples.mult_0_plus'' [in UseTactics]
EqualityExamples.mult_0_plus' [in UseTactics]
EqualityExamples.mult_0_plus [in UseTactics]
equality_by_auto [in UseAuto]
equates_6 [in LibTactics]
equates_5 [in LibTactics]
equates_4 [in LibTactics]
equates_3 [in LibTactics]
equates_2 [in LibTactics]
equates_1 [in LibTactics]
equates_0 [in LibTactics]
evalF_eval [in Smallstep]
eval__multistep [in Smallstep]
eval_assign [in PE]
ExamplesInstantiations.substitution_preserves_typing [in UseTactics]
ExamplesLets.demo_lets_underscore [in UseTactics]
ExamplesLets.demo_lets_5 [in UseTactics]
ExamplesLets.demo_lets_4 [in UseTactics]
ExamplesLets.demo_lets_3 [in UseTactics]
ExamplesLets.demo_lets_2 [in UseTactics]
ExamplesLets.demo_lets_1 [in UseTactics]

F

False_and_P_imp [in HoareAsLogic]
false_eqb_string [in Maps]
fib_eqn [in Hoare2]
find_parity_correct' [in Hoare2]
find_parity_correct [in Hoare2]
fold_constants_com_sound [in Equiv]
fold_constants_bexp_sound [in Equiv]
fold_constants_aexp_sound [in Equiv]
free_in_context [in Norm]
free_in_context [in Sub]
free_in_context [in RecordSub]

G

GenExample.substitution_preserves_typing [in UseTactics]

H

I

identity_assignment [in Equiv]
iff_trans [in Equiv]
iff_intro_swap [in LibTactics]
if_minus_plus [in Hoare]
if_minus_correct [in Hoare2]
if_minus_plus_correct [in Hoare2]
If1.hoare_if1_good [in Hoare]
inbP [in PE]
induct_height_max2 [in LibTactics]
inequiv_exercise [in Equiv]
instantiation_drop [in Norm]
instantiation_R [in Norm]
instantiation_env_closed [in Norm]
instantiation_domains_match [in Norm]
IntrovExamples.ceval_deterministic' [in UseTactics]
IntrovExamples.ceval_deterministic [in UseTactics]
IntrovExamples.dist_exists_or [in UseTactics]
IntrovExamples.exists_impl [in UseTactics]
InvertsExamples.ceval_deterministic' [in UseTactics]
InvertsExamples.ceval_deterministic [in UseTactics]
InvertsExamples.skip_left' [in UseTactics]
InvertsExamples.skip_left [in UseTactics]
is_wp_example [in Hoare2]

L

lookup_field_in_value [in RecordSub]
loop_unrolling [in Equiv]
loop_never_stops [in Imp]
Loop.ceval_count_sound [in PE]
Loop.ceval_count_complete [in PE]
Loop.pe_com_correct [in PE]
Loop.pe_com_sound [in PE]
Loop.pe_com_complete [in PE]
Loop.pe_ceval_count_le [in PE]
Loop.pe_compare_nil_update [in PE]
Loop.pe_compare_nil_lookup [in PE]
ltac_something_show [in LibTactics]
ltac_something_hide [in LibTactics]
ltac_something_eq [in LibTactics]
ltac_database_provide [in LibTactics]
l1 [in Hoare2]
l2 [in Hoare2]
l3 [in Hoare2]
l3' [in Hoare2]
l4 [in Hoare2]

M

msubst_R [in Norm]
msubst_preserves_typing [in Norm]
msubst_app [in Norm]
msubst_abs [in Norm]
msubst_var [in Norm]
msubst_closed [in Norm]
multistep__eval [in Smallstep]
multistep_congr_2 [in Smallstep]
multistep_congr_1 [in Smallstep]
multistep_App2 [in Norm]
multistep_preserves_R' [in Norm]
multistep_preserves_R [in Norm]
multi_trans [in Smallstep]
multi_R [in Smallstep]
mupdate_drop [in Norm]
mupdate_lookup [in Norm]

N

NaryExamples.demo_branch [in UseTactics]
NaryExamples.demo_splits [in UseTactics]
nat_le_refl [in UseAuto]
nat_canonical [in Types]
negation_study_2 [in UseAuto]
negation_study_1 [in UseAuto]
nf_same_as_value [in Smallstep]
nf_is_value [in Smallstep]
normalization [in Norm]
normalize_ex' [in Smallstep]
normalize_ex [in Smallstep]
normal_forms_unique [in Smallstep]
no_whiles_eqv [in Imp]

O

omega_demo_4 [in UseAuto]
omega_demo_3 [in UseAuto]
omega_demo_2 [in UseAuto]
omega_demo_1 [in UseAuto]
order_matters_2 [in UseAuto]
order_matters_1 [in UseAuto]

P

R

rcd_types_match [in RecordSub]
reduce_to_zero_correct' [in Hoare2]
refl_cequiv [in Equiv]
refl_bequiv [in Equiv]
refl_aequiv [in Equiv]
RepeatExercise.ex1_repeat_works [in Hoare]
RingDemo.ring_demo [in UseAuto]
R_typable_empty [in Norm]
R_halts [in Norm]

S

T

U

UnfoldsExample.bexp_eval_true [in UseTactics]
update_permute [in Maps]
update_same [in Maps]
update_shadow [in Maps]
update_neq [in Maps]
update_eq [in Maps]

V

vacuous_substitution [in Norm]
value_is_nf [in Smallstep]
value_halts [in Norm]
value__normal [in Norm]
value_is_nf [in Types]
verification_correct_dec [in Hoare2]
verification_correct [in Hoare2]

W

wf_rcd_lookup [in RecordSub]
WHILE_true [in Equiv]
WHILE_true_nonterm [in Equiv]
WHILE_false [in Equiv]
working_of_auto_2 [in UseAuto]
working_of_auto_1 [in UseAuto]
wp_is_weakest [in HoareAsLogic]
wp_is_precondition [in HoareAsLogic]

Z

zprop_preserving [in Equiv]

Axiom Index

E

EqualityExamples.big_expression_using [in UseTactics]
ExamplesLets.typing_inversion_var [in UseTactics]

G

gt_not_le [in UseAuto]

I

inj_pair2 [in LibTactics]

L

le_gt_false [in UseAuto]
le_not_gt [in UseAuto]

P

P [in UseAuto]

S

subtype [in UseAuto]
subtype_trans [in UseAuto]
subtype_refl [in UseAuto]

T

typ [in UseAuto]

Constructor Index

A

B

BAnd [in Imp]
Base [in Sub]
Base [in RecordSub]
BEq [in Imp]
BFalse [in Imp]
BLe [in Imp]
BNot [in Imp]
body [in PE]
Bool [in Norm]
Bool [in Sub]
Bool [in Types]
boxer [in LibTactics]
BreakImp.CAss [in Imp]
BreakImp.CBreak [in Imp]
BreakImp.CIf [in Imp]
BreakImp.CSeq [in Imp]
BreakImp.CSkip [in Imp]
BreakImp.CWhile [in Imp]
BreakImp.E_Skip [in Imp]
BreakImp.SBreak [in Imp]
BreakImp.SContinue [in Imp]
BS_AndFalse [in Smallstep]
BS_AndTrueFalse [in Smallstep]
BS_AndTrueTrue [in Smallstep]
BS_AndStep [in Smallstep]
BS_AndTrueStep [in Smallstep]
BS_NotFalse [in Smallstep]
BS_NotTrue [in Smallstep]
BS_NotStep [in Smallstep]
BS_LtEq [in Smallstep]
BS_LtEq2 [in Smallstep]
BS_LtEq1 [in Smallstep]
BS_Eq [in Smallstep]
BS_Eq2 [in Smallstep]
BS_Eq1 [in Smallstep]
BTrue [in Imp]
bv_fls [in Types]
bv_tru [in Types]

C

D

DCAsgn [in Hoare2]
DCIf [in Hoare2]
DCPost [in Hoare2]
DCPre [in Hoare2]
DCSeq [in Hoare2]
DCSkip [in Hoare2]
DCWhile [in Hoare2]
Decorated [in Hoare2]
done [in PE]

E

entry [in PE]
ev_SS [in Hoare2]
ev_0 [in Hoare2]
E_Plus [in Smallstep]
E_Const [in Smallstep]
E_WhileTrue [in Imp]
E_WhileFalse [in Imp]
E_IfFalse [in Imp]
E_IfTrue [in Imp]
E_Seq [in Imp]
E_Ass [in Imp]
E_Skip [in Imp]
E_Some [in PE]
E_None [in PE]

F

fls [in Norm]
fls [in Sub]
fls [in Types]
fst [in Norm]

G

Goto [in PE]

H

I

If [in PE]
If1.CAss [in Hoare]
If1.CIf [in Hoare]
If1.CIf1 [in Hoare]
If1.CSeq [in Hoare]
If1.CSkip [in Hoare]
If1.CWhile [in Hoare]
If1.E_WhileTrue [in Hoare]
If1.E_WhileFalse [in Hoare]
If1.E_IfFalse [in Hoare]
If1.E_IfTrue [in Hoare]
If1.E_Seq [in Hoare]
If1.E_Ass [in Hoare]
If1.E_Skip [in Hoare]
iszro [in Types]

L

loop [in PE]
Loop.E'Ass [in PE]
Loop.E'IfFalse [in PE]
Loop.E'IfTrue [in PE]
Loop.E'Seq [in PE]
Loop.E'Skip [in PE]
Loop.E'WhileFalse [in PE]
Loop.E'WhileTrue [in PE]
Loop.pe_ceval_count_intro [in PE]
Loop.PE_WhileFixed [in PE]
Loop.PE_WhileFixedLoop [in PE]
Loop.PE_WhileFixedEnd [in PE]
Loop.PE_While [in PE]
Loop.PE_WhileTrue [in PE]
Loop.PE_WhileFalse [in PE]
Loop.PE_If [in PE]
Loop.PE_IfFalse [in PE]
Loop.PE_IfTrue [in PE]
Loop.PE_Seq [in PE]
Loop.PE_AssDynamic [in PE]
Loop.PE_AssStatic [in PE]
Loop.PE_Skip [in PE]
ltac_goal_to_discard_intro [in LibTactics]
ltac_database_token [in LibTactics]
ltac_mark [in LibTactics]
ltac_wilds [in LibTactics]
ltac_wild [in LibTactics]
ltac_no_arg [in LibTactics]

M

multi_step [in Smallstep]
multi_refl [in Smallstep]

N

Nat [in Types]
nv_scc [in Types]
nv_zro [in Types]

P

P [in Smallstep]
pair [in Norm]
pe_peval_intro [in PE]
pe_ceval_intro [in PE]
PE_If [in PE]
PE_IfFalse [in PE]
PE_IfTrue [in PE]
PE_Seq [in PE]
PE_AssDynamic [in PE]
PE_AssStatic [in PE]
PE_Skip [in PE]
prd [in Types]
Prod [in Norm]

R

S

T

U

unit [in Sub]
Unit [in Sub]

V

var [in Norm]
var [in Sub]
var [in RecordSub]
VNUId [in Equiv]
VNUMinus [in Equiv]
VNUMult [in Equiv]
VNUNum [in Equiv]
VNUPlus [in Equiv]
v_const [in Smallstep]
V_cons [in Norm]
V_nil [in Norm]
v_fls [in Norm]
v_tru [in Norm]
v_pair [in Norm]
v_abs [in Norm]
v_unit [in Sub]
v_false [in Sub]
v_true [in Sub]
v_abs [in Sub]
v_rcons [in RecordSub]
v_rnil [in RecordSub]
v_abs [in RecordSub]

W

wfArrow [in RecordSub]
wfBase [in RecordSub]
wfRCons [in RecordSub]
wfRNil [in RecordSub]
wfTop [in RecordSub]

Z

zro [in Types]

Inductive Index

A

aevalR_extended.aevalR [in Imp]
aevalR_extended.aexp [in Imp]
aevalR_division.aevalR [in Imp]
aevalR_division.aexp [in Imp]
aexp [in Imp]
AExp.aevalR [in Imp]
AExp.aevalR_first_try.TooHardToRead.aevalR [in Imp]
AExp.aevalR_first_try.aevalR [in Imp]
AExp.aexp [in Imp]
AExp.bevalR [in Imp]
AExp.bexp [in Imp]
appears_free_in [in Norm]
appears_free_in [in Sub]
appears_free_in [in RecordSub]
astep [in Smallstep]
aval [in Smallstep]

B

bexp [in Imp]
block [in PE]
Boxer [in LibTactics]
BreakImp.ceval [in Imp]
BreakImp.com [in Imp]
BreakImp.result [in Imp]
bstep [in Smallstep]
bvalue [in Types]

C

ceval [in Imp]
CImp.com [in Smallstep]
CImp.cstep [in Smallstep]
com [in Imp]
Combined.step [in Smallstep]
Combined.tm [in Smallstep]
Combined.value [in Smallstep]
cstep [in Smallstep]

D

dcom [in Hoare2]
decorated [in Hoare2]

E

ev [in Hoare2]
eval [in Smallstep]

H

has_type [in Norm]
has_type [in Sub]
has_type [in RecordSub]
has_type [in Types]
Himp.ceval [in Equiv]
Himp.ceval [in Hoare]
Himp.com [in Equiv]
Himp.com [in Hoare]
HoareAssertAssume.ceval [in Hoare]
HoareAssertAssume.com [in Hoare]
HoareAssertAssume.result [in Hoare]
hoare_proof [in HoareAsLogic]

I

If1.ceval [in Hoare]
If1.com [in Hoare]
instantiation [in Norm]

L

Loop.ceval_count [in PE]
Loop.pe_ceval_count [in PE]
Loop.pe_com [in PE]
ltac_goal_to_discard [in LibTactics]
Ltac_database_token [in LibTactics]
ltac_Mark [in LibTactics]
ltac_Wilds [in LibTactics]
ltac_Wild [in LibTactics]
ltac_No_arg [in LibTactics]

M

multi [in Smallstep]

N

no_whilesR [in Imp]
nvalue [in Types]

P

parity_label [in PE]
peval [in PE]
pe_peval [in PE]
pe_ceval [in PE]
pe_com [in PE]

R

record_tm [in RecordSub]
record_ty [in RecordSub]
RepeatExercise.ceval [in Hoare]
RepeatExercise.com [in Hoare]

S

T

Temp1.step [in Smallstep]
Temp1.value [in Smallstep]
Temp2.step [in Smallstep]
Temp2.value [in Smallstep]
Temp3.step [in Smallstep]
Temp3.value [in Smallstep]
Temp4.step [in Smallstep]
Temp4.Temp5.step [in Smallstep]
Temp4.tm [in Smallstep]
Temp4.value [in Smallstep]
tm [in Smallstep]
tm [in Norm]
tm [in Sub]
tm [in RecordSub]
tm [in Types]
ty [in Norm]
ty [in Sub]
ty [in RecordSub]
ty [in Types]

V

value [in Smallstep]
value [in Norm]
value [in Sub]
value [in RecordSub]
var_not_used_in_aexp [in Equiv]

W

well_formed_ty [in RecordSub]

Section Index

D

DemoAbsurd1 [in UseAuto]

E

equatesLemma [in LibTactics]

H

HintsTransitivity [in UseAuto]

Abbreviation Index

E

Examples.A [in Sub]
Examples.A [in RecordSub]
Examples.B [in Sub]
Examples.B [in RecordSub]
Examples.C [in Sub]
Examples.C [in RecordSub]
Examples.Float [in Sub]
Examples.i [in RecordSub]
Examples.Integer [in Sub]
Examples.j [in RecordSub]
Examples.k [in RecordSub]
Examples.String [in Sub]
Examples.x [in Sub]
Examples.x [in RecordSub]
Examples.y [in Sub]
Examples.y [in RecordSub]
Examples.z [in Sub]
Examples.z [in RecordSub]

M

multistep [in Norm]

S

Definition Index

A

aequiv [in Equiv]
aeval [in Imp]
AExp.aeval [in Imp]
AExp.beval [in Imp]
AExp.manual_grade_for_beval_rules [in Imp]
AExp.optimize_0plus_b [in Imp]
AExp.optimize_0plus [in Imp]
AExp.silly_presburger_example [in Imp]
AExp.test_optimize_0plus [in Imp]
AExp.test_aeval1 [in Imp]
aexp1 [in Imp]
Assertion [in Hoare]
assert_implies [in Hoare]
assign [in PE]
assigned [in PE]
assn_sub_example2 [in Hoare]
assn_sub_example [in Hoare]
assn_sub [in Hoare]
atrans_sound [in Equiv]

B

bassn [in Hoare]
bequiv [in Equiv]
beval [in Imp]
bexp1 [in Imp]
bool_to_bexp [in Imp]
btrans_sound [in Equiv]

C

capprox [in Equiv]
cequiv [in Equiv]
ceval_example2 [in Imp]
ceval_example1 [in Imp]
ceval_fun_no_while [in Imp]
CImp.cmultistep [in Smallstep]
CImp.par_loop_example_2 [in Smallstep]
CImp.par_loop_example_0 [in Smallstep]
CImp.par_loop [in Smallstep]
closed [in Norm]
closed_env [in Norm]
cmin [in Equiv]
COIND [in LibTactics]
compiler_is_correct_statement [in Smallstep]
congruence_example [in Equiv]
context [in Norm]
context [in Sub]
context [in RecordSub]
ctrans_sound [in Equiv]
c3 [in Equiv]
c4 [in Equiv]

D

dec_correct [in Hoare2]
dec_while [in Hoare2]
dec0 [in Hoare2]
dec1 [in Hoare2]
deterministic [in Smallstep]
dfib [in Hoare2]
div_mod_dec [in Hoare2]
dpow2_down [in Hoare2]
drop [in Norm]

E

F

fact_in_coq [in Imp]
fib [in Hoare2]
find_parity_dec' [in Hoare2]
find_parity_dec [in Hoare2]
find_parity [in Hoare2]
FirstTry.type_check [in Typechecking]
fold_com_ex1 [in Equiv]
fold_constants_com [in Equiv]
fold_bexp_ex2 [in Equiv]
fold_bexp_ex1 [in Equiv]
fold_constants_bexp [in Equiv]
fold_aexp_ex2 [in Equiv]
fold_aexp_ex1 [in Equiv]
fold_constants_aexp [in Equiv]

H

halts [in Norm]
has_type_not [in Types]
has_type_1 [in Types]
Himp.cequiv [in Equiv]
Himp.havoc_example2 [in Equiv]
Himp.havoc_example1 [in Equiv]
Himp.havoc_pre [in Hoare]
Himp.hoare_triple [in Hoare]
Himp.manual_grade_for_Check_rule_for_HAVOC [in Equiv]
Himp.pcopy [in Equiv]
Himp.ptwice [in Equiv]
Himp.pXY [in Equiv]
Himp.pYX [in Equiv]
Himp.p1 [in Equiv]
Himp.p2 [in Equiv]
Himp.p3 [in Equiv]
Himp.p4 [in Equiv]
Himp.p5 [in Equiv]
Himp.p6 [in Equiv]
HoareAssertAssume.assert_assume_example [in Hoare]
HoareAssertAssume.hoare_triple [in Hoare]
hoare_asgn_example4 [in Hoare]
hoare_asgn_example3 [in Hoare]
hoare_asgn_example1' [in Hoare]
hoare_asgn_example1 [in Hoare]
hoare_triple [in Hoare]

I

if_example [in Hoare]
if_minus_dec [in Hoare2]
if_minus_plus_dec [in Hoare2]
if_minus_plus_com [in Hoare2]
If1.hoare_triple [in Hoare]
inb [in PE]
InvertsExamples.typing_nonexample_1 [in UseTactics]
is_wp [in Hoare2]

K

keval [in PE]
keval_example [in PE]

L

lookup [in Norm]
loop [in Imp]
Loop.pe_loop_example4 [in PE]
Loop.pe_loop_example3 [in PE]
Loop.pe_loop_example2 [in PE]
Loop.pe_loop_example1 [in PE]
Loop.square_loop [in PE]
ltac_something [in LibTactics]
ltac_to_generalize [in LibTactics]
ltac_tag_subst [in LibTactics]
ltac_int_to_nat [in LibTactics]
ltac_database [in LibTactics]

M

manual_grade_for_combined_properties [in Smallstep]
manual_grade_for_eval__multistep_inf [in Smallstep]
manual_grade_for_equiv_classes [in Equiv]
manual_grade_for_no_whiles_terminating [in Imp]
manual_grade_for_XtimesYinZ_spec [in Imp]
manual_grade_for_norm [in Norm]
manual_grade_for_norm_fail [in Norm]
manual_grade_for_products [in Sub]
manual_grade_for_variations [in Sub]
manual_grade_for_pair_permutation [in Sub]
manual_grade_for_smallest_2 [in Sub]
manual_grade_for_smallest_1 [in Sub]
manual_grade_for_small_large_4 [in Sub]
manual_grade_for_small_large_2 [in Sub]
manual_grade_for_small_large_1 [in Sub]
manual_grade_for_proper_subtypes [in Sub]
manual_grade_for_subtype_concepts_tf [in Sub]
manual_grade_for_subtype_instances_tf_2 [in Sub]
manual_grade_for_subtype_order [in Sub]
manual_grade_for_arrow_sub_wrong [in Sub]
manual_grade_for_hoare_repeat [in Hoare]
manual_grade_for_if1_hoare [in Hoare]
manual_grade_for_hoarestate1 [in Hoare]
manual_grade_for_hoare_asgn_examples_2 [in Hoare]
manual_grade_for_hoare_asgn_wrong [in Hoare]
manual_grade_for_hoare_asgn_examples [in Hoare]
manual_grade_for_rcd_types_match_informal [in RecordSub]
manual_grade_for_factorial_dec [in Hoare2]
manual_grade_for_check_defn_of_slow_assignment_dec [in Hoare2]
manual_grade_for_decorations_in_two_loops [in Hoare2]
manual_grade_for_decorations_in_Min_Hoare [in Hoare2]
manual_grade_for_decorations_in_factorial [in Hoare2]
manual_grade_for_decorations_in_slow_assignment [in Hoare2]
manual_grade_for_decorations_in_if_minus_plus_reloaded [in Hoare2]
manual_grade_for_prog_pres_bigstep [in Types]
manual_grade_for_remove_predzro [in Types]
manual_grade_for_variation2 [in Types]
manual_grade_for_variation1 [in Types]
manual_grade_for_subject_expansion [in Types]
manual_grade_for_finish_preservation_informal [in Types]
manual_grade_for_finish_progress_informal [in Types]
msubst [in Norm]
multistep [in Types]
mupdate [in Norm]
myFact [in UseAuto]

N

normalizing [in Smallstep]
normal_form_of [in Smallstep]
normal_form [in Smallstep]
no_whiles [in Imp]

P

parity [in PE]
parity [in Hoare2]
parity_eval [in PE]
parity_body [in PE]
parity_dec [in Hoare2]
partial_map [in Maps]
pe_program [in PE]
pe_block_example [in PE]
pe_block [in PE]
pe_example3 [in PE]
pe_example2 [in PE]
pe_example1 [in PE]
pe_removes [in PE]
pe_compare [in PE]
pe_unique [in PE]
pe_disagree_at [in PE]
pe_add [in PE]
pe_remove [in PE]
pe_bexp [in PE]
pe_update [in PE]
pe_consistent [in PE]
pe_aexp [in PE]
pe_lookup [in PE]
pe_state [in PE]
plus2 [in Imp]
post [in Hoare2]
post_dec [in Hoare2]
pow2 [in Hoare2]
pre_dec [in Hoare2]
prog [in Smallstep]
program [in PE]
prog_i [in Equiv]
prog_h [in Equiv]
prog_g [in Equiv]
prog_f [in Equiv]
prog_e [in Equiv]
prog_d [in Equiv]
prog_c [in Equiv]
prog_b [in Equiv]
prog_a [in Equiv]
pup_to_n [in Imp]

R

R [in Norm]
real_fact [in Hoare2]
reduce_to_zero' [in Hoare2]
relation [in Smallstep]
RepeatExercise.ex1_repeat [in Hoare]
RepeatExercise.hoare_triple [in Hoare]
rm [in LibTactics]

S

T

T [in Hoare2]
tass [in Norm]
Temp4.bool_step_prop3 [in Smallstep]
Temp4.bool_step_prop2 [in Smallstep]
Temp4.bool_step_prop1 [in Smallstep]
Temp4.manual_grade_for_smallstep_bools [in Smallstep]
Temp4.Temp5.bool_step_prop4_holds [in Smallstep]
Temp4.Temp5.bool_step_prop4 [in Smallstep]
test_pe_bexp2 [in PE]
test_pe_bexp1 [in PE]
test_pe_update [in PE]
test_pe_aexp1 [in PE]
text_pe_aexp2 [in PE]
tlookup [in RecordSub]
Tlookup [in RecordSub]
total_map [in Maps]
two_loops_dec [in Hoare2]
TypecheckerExtensions.eqb_ty [in Typechecking]
TypecheckerExtensions.manual_grade_for_type_checking_complete [in Typechecking]
TypecheckerExtensions.manual_grade_for_type_checking_sound [in Typechecking]
TypecheckerExtensions.type_check [in Typechecking]
t_update [in Maps]
t_empty [in Maps]

U

update [in Maps]
update_example4 [in Maps]
update_example3 [in Maps]
update_example2 [in Maps]
update_example1 [in Maps]

V

value [in Types]
verification_conditions_dec [in Hoare2]
verification_conditions [in Hoare2]

W

W [in Imp]
while_example [in Hoare]
wp [in HoareAsLogic]

X

X [in Imp]
XtimesYinZ [in Imp]

Y

Y [in Imp]

Z

Z [in Imp]
zprop [in Equiv]

Global Index

other

(2142 entries)

Notation Index

other

(161 entries)

Module Index

other

(71 entries)

Variable Index

other

(7 entries)

Library Index

other

(24 entries)

Lemma Index

other

(496 entries)

Axiom Index

other

(11 entries)

Constructor Index

other

(749 entries)

Inductive Index

other

(140 entries)

Section Index

other

(3 entries)

Abbreviation Index

other

(55 entries)

Definition Index

other

(425 entries)