Global Index

(2854 entries)

Notation Index

(174 entries)

Module Index

(82 entries)

Variable Index

(8 entries)

Library Index

(39 entries)

Lemma Index

(768 entries)

Constructor Index

(854 entries)

Axiom Index

(12 entries)

Inductive Index

(184 entries)

Section Index

(3 entries)

Abbreviation Index

(55 entries)

Definition Index

(675 entries)

Global Index

A

abs_arrow [lemma, in RecordSub]
abs_arrow [lemma, in Sub]
add1 [definition, in ProofObjects]
admit [definition, in Basics]
aequiv [definition, in Equiv]
aequiv_example [lemma, in Equiv]
aeval [definition, in Imp]
aevalR_division [module, in Imp]
aevalR_division.ADiv [constructor, in Imp]
aevalR_division.aevalR [inductive, in Imp]
aevalR_division.aexp [inductive, in Imp]
aevalR_division.AMinus [constructor, in Imp]
aevalR_division.AMult [constructor, in Imp]
aevalR_division.ANum [constructor, in Imp]
aevalR_division.APlus [constructor, in Imp]
aevalR_division.E_ADiv [constructor, in Imp]
aevalR_division.E_AMinus [constructor, in Imp]
aevalR_division.E_AMult [constructor, in Imp]
aevalR_division.E_ANum [constructor, in Imp]
aevalR_division.E_APlus [constructor, in Imp]
aevalR_division.:type_scope:x_'\\'_x [notation, in Imp]
aevalR_extended [module, in Imp]
aevalR_extended.AAny [constructor, in Imp]
aevalR_extended.aevalR [inductive, in Imp]
aevalR_extended.aexp [inductive, in Imp]
aevalR_extended.AMinus [constructor, in Imp]
aevalR_extended.AMult [constructor, in Imp]
aevalR_extended.ANum [constructor, in Imp]
aevalR_extended.APlus [constructor, in Imp]
aevalR_extended.E_AMinus [constructor, in Imp]
aevalR_extended.E_AMult [constructor, in Imp]
aevalR_extended.E_ANum [constructor, in Imp]
aevalR_extended.E_Any [constructor, in Imp]
aevalR_extended.E_APlus [constructor, in Imp]
aevalR_extended.:type_scope:x_'\\'_x [notation, 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]
AExp.aevalR_first_try [module, in Imp]
AExp.aevalR_first_try.aevalR [inductive, in Imp]
AExp.aevalR_first_try.E_AMinus [constructor, in Imp]
AExp.aevalR_first_try.E_AMult [constructor, in Imp]
AExp.aevalR_first_try.E_ANum [constructor, in Imp]
AExp.aevalR_first_try.E_APlus [constructor, in Imp]
AExp.aevalR_first_try.:type_scope:x_'\\'_x [notation, 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.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_AMinus [constructor, in Imp]
AExp.E_AMult [constructor, in Imp]
AExp.E_ANum [constructor, in Imp]
AExp.E_APlus [constructor, in Imp]
AExp.foo [lemma, in Imp]
AExp.foo' [lemma, in Imp]
AExp.In10 [lemma, in Imp]
AExp.In10' [lemma, in Imp]
AExp.optimize_0plus [definition, in Imp]
AExp.optimize_0plus_b [definition, in Imp]
AExp.optimize_0plus_b_sound [lemma, in Imp]
AExp.optimize_0plus_sound [lemma, in Imp]
AExp.optimize_0plus_sound' [lemma, in Imp]
AExp.optimize_0plus_sound'' [lemma, in Imp]
AExp.silly1 [lemma, in Imp]
AExp.silly2 [lemma, in Imp]
AExp.silly_presburger_example [definition, in Imp]
AExp.test_aeval1 [definition, in Imp]
AExp.test_optimize_0plus [definition, in Imp]
AExp.:type_scope:x_'\\'_x [notation, in Imp]
aexp1 [definition, in Imp]
afi_abs [constructor, in Sub]
afi_abs [constructor, in Norm]
afi_abs [constructor, in RecordSub]
afi_app1 [constructor, in Norm]
afi_app1 [constructor, in RecordSub]
afi_app1 [constructor, in Sub]
afi_app2 [constructor, in Norm]
afi_app2 [constructor, in RecordSub]
afi_app2 [constructor, in Sub]
afi_fst [constructor, in Norm]
afi_if₀ [constructor, in Norm]
afi_if₁ [constructor, in Sub]
afi_if₁ [constructor, in Norm]
afi_if₂ [constructor, in Sub]
afi_if₂ [constructor, in Norm]
afi_if₃ [constructor, in Sub]
afi_pair1 [constructor, in Norm]
afi_pair2 [constructor, in Norm]
afi_proj [constructor, in RecordSub]
afi_rhead [constructor, in RecordSub]
afi_rtail [constructor, in RecordSub]
afi_snd [constructor, in Norm]
afi_var [constructor, in Sub]
afi_var [constructor, in RecordSub]
afi_var [constructor, in Norm]
AId [constructor, in Imp]
All [definition, in Logic]
all3_spec [lemma, in Induction]
All_In [lemma, in Logic]
alpha [constructor, in ImpParser]
always_loop_hoare [lemma, in Hoare]
AMinus [constructor, in Imp]
AMult [constructor, in Imp]
andb [definition, in Basics]
andb3 [definition, in Basics]
andb3_exchange [lemma, in Basics]
andb_commutative [lemma, in Basics]
andb_commutative' [lemma, in Basics]
andb_commutative'' [lemma, in Basics]
andb_eq_orb [lemma, in Basics]
andb_false_r [lemma, in Induction]
andb_true_elim2 [lemma, in Basics]
andb_true_iff [lemma, in Logic]
and_assoc [lemma, in Logic]
and_commut [lemma, in Logic]
and_example [definition, in Logic]
and_example' [definition, in Logic]
and_example2 [lemma, in Logic]
and_example2' [lemma, in Logic]
and_example2'' [lemma, in Logic]
and_example3 [lemma, in Logic]
and_exercise [definition, in Logic]
and_intro [lemma, in Logic]
antisymmetric [definition, in Rel]
ANum [constructor, in Imp]
APlus [constructor, in Imp]
app [definition, in Poly]
App [constructor, in IndProp]
appears_free_in [inductive, in Sub]
appears_free_in [inductive, in Norm]
appears_free_in [inductive, in RecordSub]
apply_empty [lemma, in Maps]
apply_iff_example [lemma, in Logic]
app_assoc [lemma, in Poly]
app_length [lemma, in Poly]
app_length_cons [lemma, in Tactics]
app_length_twice [lemma, in Tactics]
app_nil_r [lemma, in Poly]
Assertion [definition, in Hoare]
assert_implies [definition, in Hoare]
assign [definition, in PE]
Assign [constructor, in PE]
assigned [definition, in PE]
assign_aequiv [lemma, in Equiv]
assign_removes [lemma, in PE]
assn_sub [definition, in Hoare]
assn_sub_example [definition, in Hoare]
astep [inductive, in Smallstep]
astep_example1 [definition, in Types]
astep_example1' [definition, in Types]
astep_example1'' [definition, in Types]
astep_example1''' [definition, in Types]
AS_Id [constructor, in Smallstep]
AS_Minus [constructor, in Smallstep]
AS_Minus1 [constructor, in Smallstep]
AS_Minus2 [constructor, in Smallstep]
AS_Mult [constructor, in Smallstep]
AS_Mult1 [constructor, in Smallstep]
AS_Mult2 [constructor, in Smallstep]
AS_Plus [constructor, in Smallstep]
AS_Plus1 [constructor, in Smallstep]
AS_Plus2 [constructor, in Smallstep]
atrans_sound [definition, in Equiv]
Auto [library]
auto_example_1 [definition, in Auto]
auto_example_1' [definition, in Auto]
auto_example_2 [definition, in Auto]
auto_example_3 [definition, in Auto]
auto_example_4 [definition, in Auto]
auto_example_5 [definition, in Auto]
auto_example_6 [definition, in Auto]
auto_example_6' [definition, in Auto]
auto_example_7 [definition, in Auto]
auto_example_7' [definition, in Auto]
auto_example_8 [definition, in Auto]
auto_example_8' [definition, in Auto]
aval [inductive, in Smallstep]
av_num [constructor, in Smallstep]

B

BAnd [constructor, in Imp]
bar [definition, in Tactics]
Basics [library]
bassn [definition, in Hoare]
bassn_eval_false [lemma, in HoareAsLogic]
baz [inductive, in Lists]
Baz1 [constructor, in Lists]
Baz2 [constructor, in Lists]
bempty [constructor, in IndPrinciples]
BEq [constructor, in Imp]
bequiv [definition, in Equiv]
bequiv_example [lemma, in Equiv]
beq_id [definition, in Maps]
beq_id [definition, in Lists]
beq_idP [lemma, in Maps]
beq_id_false_iff [lemma, in Maps]
beq_id_refl [lemma, in Lists]
beq_id_refl [lemma, in Maps]
beq_id_true [lemma, in Tactics]
beq_id_true_iff [lemma, in Maps]
beq_list [definition, in Logic]
beq_list_true_iff [lemma, in Logic]
beq_nat [definition, in Basics]
beq_natP [lemma, in IndProp]
beq_nat_false_iff [lemma, in Logic]
beq_nat_refl [lemma, in Induction]
beq_nat_sym [lemma, in Tactics]
beq_nat_trans [lemma, in Tactics]
beq_nat_true [lemma, in Tactics]
beq_nat_true_iff [lemma, in Logic]
beq_nat_0_l [lemma, in Tactics]
beval [definition, in Imp]
bexp [inductive, in Imp]
bexp1 [definition, in Imp]
bexp_eval_false [lemma, in Hoare]
bexp_eval_true [lemma, in Hoare]
BFalse [constructor, in Imp]
Bib [library]
bignumber [definition, in ImpParser]
BLe [constructor, in Imp]
bleaf [constructor, in IndPrinciples]
block [inductive, in PE]
blt_nat [definition, in Basics]
blue [constructor, in IndPrinciples]
BNot [constructor, in Imp]
body [constructor, in PE]
bool [inductive, in Basics]
boollist [inductive, in Poly]
bool_canonical [lemma, in Types]
bool_cons [constructor, in Poly]
bool_fn_applied_thrice [lemma, in Tactics]
bool_nil [constructor, in Poly]
Boxer [inductive, in LibTactics]
boxer [constructor, 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.SBreak [constructor, in Imp]
BreakImp.SContinue [constructor, in Imp]
BreakImp.status [inductive, in Imp]
BreakImp.while_break_true [lemma, in Imp]
BreakImp.while_continue [lemma, in Imp]
BreakImp.while_stops_on_break [lemma, in Imp]
BreakImp.::x_'/'_x_'\\'_x_'/'_x [notation, in Imp]
BreakImp.::x_'::='_x [notation, in Imp]
BreakImp.::x_';;'_x [notation, in Imp]
BreakImp.::'BREAK' [notation, in Imp]
BreakImp.::'IFB'_x_'THEN'_x_'ELSE'_x_'FI' [notation, in Imp]
BreakImp.::'SKIP' [notation, in Imp]
BreakImp.::'WHILE'_x_'DO'_x_'END' [notation, in Imp]
bstep [inductive, in Smallstep]
BS_AndFalse [constructor, in Smallstep]
BS_AndStep [constructor, in Smallstep]
BS_AndTrueFalse [constructor, in Smallstep]
BS_AndTrueStep [constructor, in Smallstep]
BS_AndTrueTrue [constructor, in Smallstep]
BS_Eq [constructor, in Smallstep]
BS_Eq₁ [constructor, in Smallstep]
BS_Eq₂ [constructor, in Smallstep]
BS_LtEq [constructor, in Smallstep]
BS_LtEq1 [constructor, in Smallstep]
BS_LtEq2 [constructor, in Smallstep]
BS_NotFalse [constructor, in Smallstep]
BS_NotStep [constructor, in Smallstep]
BS_NotTrue [constructor, in Smallstep]
btrans_sound [definition, in Equiv]
BTrue [constructor, in Imp]
build_symtable [definition, in ImpParser]
bvalue [inductive, in Types]
bv_false [constructor, in Types]
bv_true [constructor, in Types]
byntree [inductive, in IndPrinciples]

C

D

E

F

G

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

H

I

K

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

L

M

many [definition, in ImpParser]
many_helper [definition, in ImpParser]
map [definition, in Poly]
MApp [constructor, in IndProp]
Maps [library]
map_rev [lemma, in Poly]
MChar [constructor, in IndProp]
MEmpty [constructor, in IndProp]
minustwo [definition, in Basics]
minus_diag [lemma, in Induction]
monday [constructor, in Basics]
MoreStlc [library]
MStarApp [constructor, in IndProp]
MStar' [lemma, in IndProp]
MStar'' [lemma, in IndProp]
MStar0 [constructor, in IndProp]
MStar1 [lemma, in IndProp]
msubst [definition, in Norm]
msubst_abs [lemma, in Norm]
msubst_app [lemma, in Norm]
msubst_closed [lemma, in Norm]
msubst_preserves_typing [lemma, in Norm]
msubst_R [lemma, in Norm]
msubst_var [lemma, in Norm]
multi [inductive, in Smallstep]
multistep [abbreviation, in Norm]
multistep [definition, in Types]
multistep_App2 [lemma, in Norm]
multistep_congr_1 [lemma, in Smallstep]
multistep_congr_2 [lemma, in Smallstep]
multistep_preserves_R [lemma, in Norm]
multistep_preserves_R' [lemma, in Norm]
multistep__eval [lemma, in Smallstep]
multi_R [lemma, in Smallstep]
multi_refl [constructor, in Smallstep]
multi_step [constructor, in Smallstep]
multi_trans [lemma, in Smallstep]
mult_assoc [lemma, in Induction]
mult_comm [lemma, in Induction]
mult_eq_0 [lemma, in Logic]
mult_plus_distr_r [lemma, in Induction]
mult_S_1 [lemma, in Basics]
mult_0 [lemma, in Logic]
mult_0_l [lemma, in Basics]
mult_0_plus [lemma, in Basics]
mult_0_plus' [lemma, in Induction]
mult_0_r [lemma, in Induction]
mult_0_r' [lemma, in IndPrinciples]
mult_0_r'' [lemma, in IndPrinciples]
mult_0_3 [lemma, in Logic]
mult_1_l [lemma, in Induction]
MumbleGrumble [module, in Poly]
MumbleGrumble.a [constructor, in Poly]
MumbleGrumble.b [constructor, in Poly]
MumbleGrumble.c [constructor, in Poly]
MumbleGrumble.d [constructor, in Poly]
MumbleGrumble.e [constructor, in Poly]
MumbleGrumble.grumble [inductive, in Poly]
MumbleGrumble.mumble [inductive, in Poly]
MUnionL [constructor, in IndProp]
MUnionR [constructor, in IndProp]
MUnion' [lemma, in IndProp]
mupdate [definition, in Norm]
mupdate_drop [lemma, in Norm]
mupdate_lookup [lemma, in Norm]
MyEquality [module, in ProofObjects]
MyEquality.eq [inductive, in ProofObjects]
MyEquality.eq_refl [constructor, in ProofObjects]
MyEquality.four [lemma, in ProofObjects]
MyEquality.four' [definition, in ProofObjects]
MyEquality.leibniz_equality [lemma, in ProofObjects]
MyEquality.singleton [definition, in ProofObjects]
MyEquality.:type_scope:x_'='_x [notation, in ProofObjects]
myFact [definition, in UseAuto]
MyIff [module, in Logic]
MyIff.iff [definition, in Logic]
MyIff.:type_scope:x_'<->'_x [notation, in Logic]
mynil [definition, in Poly]
mynil [definition, in Poly]
mynil' [definition, in Poly]
MyNot [module, in Logic]
MyNot.not [definition, in Logic]
MyNot.:type_scope:'~'_x [notation, in Logic]

N

O

oddb [definition, in Basics]
omega_demo_1 [lemma, in UseAuto]
omega_demo_2 [lemma, in UseAuto]
omega_demo_3 [lemma, in UseAuto]
omega_demo_4 [lemma, in UseAuto]
one_not_even [lemma, in IndProp]
option [inductive, in Poly]
optionE [inductive, in ImpParser]
option_map [definition, in Poly]
orb [definition, in Basics]
orb_true_iff [lemma, in Logic]
order [definition, in Rel]
order_matters_1 [lemma, in UseAuto]
order_matters_2 [lemma, in UseAuto]
or_assoc [lemma, in Logic]
or_commut [lemma, in Logic]
or_distributes_over_and [lemma, in Logic]
or_example [lemma, in Logic]
or_intro [lemma, in Logic]
other [constructor, in ImpParser]
O_le_n [lemma, in IndProp]

P

Q

quiz6 [definition, in ProofObjects]

R

S

T

tabs [constructor, in RecordSub]
tabs [constructor, in Sub]
tabs [constructor, in Norm]
Tactics [library]
tapp [constructor, in Norm]
tapp [constructor, in RecordSub]
tapp [constructor, in Sub]
TArrow [constructor, in Norm]
TArrow [constructor, in RecordSub]
TArrow [constructor, in Sub]
tass [definition, in Norm]
TBase [constructor, in RecordSub]
TBase [constructor, in Sub]
TBool [constructor, in Sub]
TBool [constructor, in Types]
TBool [constructor, in Norm]
Temp1 [module, in Smallstep]
Temp1.step [inductive, in Smallstep]
Temp1.ST_PlusConstConst [constructor, in Smallstep]
Temp1.ST_Plus1 [constructor, in Smallstep]
Temp1.ST_Plus2 [constructor, in Smallstep]
Temp1.value [inductive, in Smallstep]
Temp1.value_not_same_as_normal_form [lemma, in Smallstep]
Temp1.v_const [constructor, in Smallstep]
Temp1.v_funny [constructor, in Smallstep]
Temp1.::x_'==>'_x [notation, in Smallstep]
Temp2 [module, in Smallstep]
Temp2.step [inductive, in Smallstep]
Temp2.ST_Funny [constructor, in Smallstep]
Temp2.ST_PlusConstConst [constructor, in Smallstep]
Temp2.ST_Plus1 [constructor, in Smallstep]
Temp2.ST_Plus2 [constructor, in Smallstep]
Temp2.value [inductive, in Smallstep]
Temp2.value_not_same_as_normal_form [lemma, in Smallstep]
Temp2.v_const [constructor, in Smallstep]
Temp2.::x_'==>'_x [notation, in Smallstep]
Temp3 [module, in Smallstep]
Temp3.step [inductive, in Smallstep]
Temp3.ST_PlusConstConst [constructor, in Smallstep]
Temp3.ST_Plus1 [constructor, in Smallstep]
Temp3.value [inductive, in Smallstep]
Temp3.value_not_same_as_normal_form [lemma, in Smallstep]
Temp3.v_const [constructor, in Smallstep]
Temp3.::x_'==>'_x [notation, in Smallstep]
Temp4 [module, in Smallstep]
Temp4.bool_step_prop1 [definition, in Smallstep]
Temp4.bool_step_prop2 [definition, in Smallstep]
Temp4.bool_step_prop3 [definition, in Smallstep]
Temp4.step [inductive, in Smallstep]
Temp4.step_deterministic [lemma, in Smallstep]
Temp4.strong_progress [lemma, in Smallstep]
Temp4.ST_If [constructor, in Smallstep]
Temp4.ST_IfFalse [constructor, in Smallstep]
Temp4.ST_IfTrue [constructor, in Smallstep]
Temp4.Temp5 [module, in Smallstep]
Temp4.Temp5.bool_step_prop4 [definition, in Smallstep]
Temp4.Temp5.bool_step_prop4_holds [definition, in Smallstep]
Temp4.Temp5.step [inductive, in Smallstep]
Temp4.Temp5.ST_If [constructor, in Smallstep]
Temp4.Temp5.ST_IfFalse [constructor, in Smallstep]
Temp4.Temp5.ST_IfTrue [constructor, in Smallstep]
Temp4.Temp5.::x_'==>'_x [notation, in Smallstep]
Temp4.tfalse [constructor, in Smallstep]
Temp4.tif [constructor, in Smallstep]
Temp4.tm [inductive, in Smallstep]
Temp4.ttrue [constructor, in Smallstep]
Temp4.value [inductive, in Smallstep]
Temp4.v_false [constructor, in Smallstep]
Temp4.v_true [constructor, in Smallstep]
Temp4.::x_'==>'_x [notation, in Smallstep]
testParsing [definition, in ImpParser]
test_andb31 [definition, in Basics]
test_andb32 [definition, in Basics]
test_andb33 [definition, in Basics]
test_andb34 [definition, in Basics]
test_anon_fun' [definition, in Poly]
test_blt_nat1 [definition, in Basics]
test_blt_nat2 [definition, in Basics]
test_blt_nat3 [definition, in Basics]
test_ceval [definition, in ImpCEvalFun]
test_countoddmembers'1 [definition, in Poly]
test_countoddmembers'2 [definition, in Poly]
test_countoddmembers'3 [definition, in Poly]
test_doit3times [definition, in Poly]
test_doit3times' [definition, in Poly]
test_factorial1 [definition, in Basics]
test_factorial2 [definition, in Basics]
test_filter1 [definition, in Poly]
test_filter2 [definition, in Poly]
test_filter2' [definition, in Poly]
test_filter_even_gt7_1 [definition, in Poly]
test_filter_even_gt7_2 [definition, in Poly]
test_flat_map1 [definition, in Poly]
test_hd_error1 [definition, in Poly]
test_hd_error2 [definition, in Poly]
test_leb1 [definition, in Basics]
test_leb2 [definition, in Basics]
test_leb3 [definition, in Basics]
test_length1 [definition, in Poly]
test_map1 [definition, in Poly]
test_map2 [definition, in Poly]
test_map3 [definition, in Poly]
test_multistep_1 [lemma, in Smallstep]
test_multistep_1' [lemma, in Smallstep]
test_multistep_2 [lemma, in Smallstep]
test_multistep_3 [lemma, in Smallstep]
test_multistep_4 [lemma, in Smallstep]
test_nandb1 [definition, in Basics]
test_nandb2 [definition, in Basics]
test_nandb3 [definition, in Basics]
test_nandb4 [definition, in Basics]
test_next_weekday [definition, in Basics]
test_nostutter_1 [definition, in IndProp]
test_nostutter_2 [definition, in IndProp]
test_nostutter_3 [definition, in IndProp]
test_nostutter_4 [definition, in IndProp]
test_nth_error1 [definition, in Poly]
test_nth_error2 [definition, in Poly]
test_nth_error3 [definition, in Poly]
test_oddb1 [definition, in Basics]
test_oddb2 [definition, in Basics]
test_orb1 [definition, in Basics]
test_orb2 [definition, in Basics]
test_orb3 [definition, in Basics]
test_orb4 [definition, in Basics]
test_orb5 [definition, in Basics]
test_partition1 [definition, in Poly]
test_partition2 [definition, in Poly]
test_pe_aexp1 [definition, in PE]
test_pe_bexp1 [definition, in PE]
test_pe_bexp2 [definition, in PE]
test_pe_update [definition, in PE]
test_plus3 [definition, in Poly]
test_plus3' [definition, in Poly]
test_plus3'' [definition, in Poly]
test_repeat1 [definition, in Poly]
test_repeat2 [definition, in Poly]
test_rev1 [definition, in Poly]
test_rev2 [definition, in Poly]
test_split [definition, in Poly]
text_pe_aexp2 [definition, in PE]
tfalse [constructor, in Sub]
tfalse [constructor, in Types]
tfalse [constructor, in Norm]
tfst [constructor, in Norm]
thursday [constructor, in Basics]
tif [constructor, in Types]
tif [constructor, in Norm]
tif [constructor, in Sub]
tiszero [constructor, in Types]
tlookup [definition, in RecordSub]
Tlookup [definition, in RecordSub]
tm [inductive, in Norm]
tm [inductive, in Types]
tm [inductive, in RecordSub]
tm [inductive, in Sub]
tm [inductive, in Smallstep]
TNat [constructor, in Types]
token [definition, in ImpParser]
tokenize [definition, in ImpParser]
tokenize_ex₁ [definition, in ImpParser]
tokenize_helper [definition, in ImpParser]
total_map [definition, in Maps]
tpair [constructor, in Norm]
tpred [constructor, in Types]
TProd [constructor, in Norm]
tproj [constructor, in RecordSub]
transitive [definition, in Rel]
transitivity_bad_hint_1 [lemma, in UseAuto]
transitivity_workaround_1 [lemma, in UseAuto]
transitivity_workaround_2 [lemma, in UseAuto]
trans_aequiv [lemma, in Equiv]
trans_bequiv [lemma, in Equiv]
trans_cequiv [lemma, in Equiv]
trans_eq [lemma, in Tactics]
trans_eq_example [definition, in Tactics]
trans_eq_example' [definition, in Tactics]
trans_eq_exercise [definition, in Tactics]
trcons [constructor, in RecordSub]
TRCons [constructor, in RecordSub]
tree [inductive, in IndPrinciples]
TRNil [constructor, in RecordSub]
trnil [constructor, in RecordSub]
true [constructor, in Basics]
True_is_true [lemma, in Logic]
tr_rev [definition, in Logic]
tr_rev_correct [lemma, in Logic]
tsnd [constructor, in Norm]
tsucc [constructor, in Types]
TTop [constructor, in Sub]
TTop [constructor, in RecordSub]
ttrue [constructor, in Types]
ttrue [constructor, in Sub]
ttrue [constructor, in Norm]
tuesday [constructor, in Basics]
tunit [constructor, in Sub]
TUnit [constructor, in Sub]
tvar [constructor, in RecordSub]
tvar [constructor, in Sub]
tvar [constructor, in Norm]
two_loops_correct [lemma, in Hoare2]
two_loops_dec [definition, in Hoare2]
ty [inductive, in Types]
ty [inductive, in RecordSub]
ty [inductive, in Sub]
ty [inductive, in Norm]
typ [axiom, in UseAuto]
typable_empty__closed [lemma, in Norm]
Typechecking [library]
Types [library]
typing_inversion_abs [lemma, in Sub]
typing_inversion_abs [lemma, in RecordSub]
typing_inversion_app [lemma, in RecordSub]
typing_inversion_app [lemma, in Sub]
typing_inversion_false [lemma, in Sub]
typing_inversion_if [lemma, in Sub]
typing_inversion_proj [lemma, in RecordSub]
typing_inversion_rcons [lemma, in RecordSub]
typing_inversion_true [lemma, in Sub]
typing_inversion_unit [lemma, in Sub]
typing_inversion_var [lemma, in Sub]
typing_inversion_var [lemma, in RecordSub]
tzero [constructor, in Types]
T_Abs [constructor, in RecordSub]
T_Abs [constructor, in Norm]
T_Abs [constructor, in Sub]
T_App [constructor, in Sub]
T_App [constructor, in RecordSub]
T_App [constructor, in Norm]
t_apply_empty [lemma, in Maps]
t_empty [definition, in Maps]
T_False [constructor, in Types]
T_False [constructor, in Norm]
T_False [constructor, in Sub]
T_Fst [constructor, in Norm]
T_If [constructor, in Sub]
T_If [constructor, in Types]
T_If [constructor, in Norm]
T_Iszero [constructor, in Types]
T_Pair [constructor, in Norm]
T_Pred [constructor, in Types]
T_Proj [constructor, in RecordSub]
T_RCons [constructor, in RecordSub]
T_RNil [constructor, in RecordSub]
T_Snd [constructor, in Norm]
T_Sub [constructor, in RecordSub]
T_Sub [constructor, in Sub]
T_Succ [constructor, in Types]
T_True [constructor, in Norm]
T_True [constructor, in Types]
T_True [constructor, in Sub]
T_Unit [constructor, in Sub]
t_update [definition, in Maps]
t_update_eq [lemma, in Maps]
t_update_neq [lemma, in Maps]
t_update_permute [lemma, in Maps]
t_update_same [lemma, in Maps]
t_update_shadow [lemma, in Maps]
T_Var [constructor, in Norm]
T_Var [constructor, in Sub]
T_Var [constructor, in RecordSub]
T_Zero [constructor, in Types]

U

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

V

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

W

wednesday [constructor, in Basics]
well_formed_ty [inductive, in RecordSub]
wfTArrow [constructor, in RecordSub]
wfTBase [constructor, in RecordSub]
wfTRCons [constructor, in RecordSub]
wfTRNil [constructor, in RecordSub]
wfTTop [constructor, in RecordSub]
wf_rcd_lookup [lemma, in RecordSub]
while_example [definition, in Hoare]
WHILE_false [lemma, in Equiv]
WHILE_true [lemma, in Equiv]
WHILE_true_nonterm [lemma, in Equiv]
white [constructor, in ImpParser]
working_of_auto_1 [lemma, in UseAuto]
working_of_auto_2 [lemma, in UseAuto]
wp [definition, in HoareAsLogic]
wp_is_precondition [lemma, in HoareAsLogic]
wp_is_weakest [lemma, in HoareAsLogic]
wrong_ev [inductive, in IndProp]
wrong_ev_SS [constructor, in IndProp]
wrong_ev_0 [constructor, in IndProp]

X

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

Y

Y [definition, in Imp]
yes [constructor, in IndPrinciples]
yesno [inductive, in IndPrinciples]

Z

Z [definition, in Imp]
zero_nbeq_plus_1 [lemma, in Basics]
zero_nbeq_S [lemma, in Induction]
zero_not_one [lemma, in Logic]
zero_not_one' [lemma, in Logic]
zero_or_succ [lemma, in Logic]
zprop [definition, in Equiv]
zprop_preserving [lemma, in Equiv]

:

Notation Index

A

aevalR_division.:type_scope:x_'\\'_x [in Imp]
aevalR_extended.:type_scope:x_'\\'_x [in Imp]
AExp.aevalR_first_try.:type_scope:x_'\\'_x [in Imp]
AExp.:type_scope:x_'\\'_x [in Imp]

B

BreakImp.::x_'/'_x_'\\'_x_'/'_x [in Imp]
BreakImp.::x_'::='_x [in Imp]
BreakImp.::x_';;'_x [in Imp]
BreakImp.::'BREAK' [in Imp]
BreakImp.::'IFB'_x_'THEN'_x_'ELSE'_x_'FI' [in Imp]
BreakImp.::'SKIP' [in Imp]
BreakImp.::'WHILE'_x_'DO'_x_'END' [in Imp]

C

CImp.::x_'/'_x_'==>'_x_'/'_x [in Smallstep]
CImp.::x_'/'_x_'==>*'_x_'/'_x [in Smallstep]
CImp.::x_'::='_x [in Smallstep]
CImp.::x_';;'_x [in Smallstep]
CImp.::'IFB'_x_'THEN'_x_'ELSE'_x_'FI' [in Smallstep]
CImp.::'PAR'_x_'WITH'_x_'END' [in Smallstep]
CImp.::'SKIP' [in Smallstep]
CImp.::'WHILE'_x_'DO'_x_'END' [in Smallstep]
Combined.::x_'==>'_x [in Smallstep]

H

{{'_x_'}}'_x_'{{'_x_'}}'">Himp.:hoare_spec_scope:'{{'_x_'}}'_x_'{{'_x_'}}' [in Hoare]
Himp.::x_'/'_x_'\\'_x [in Equiv]
Himp.::x_'/'_x_'\\'_x [in Hoare]
Himp.::x_'::='_x [in Equiv]
Himp.::x_'::='_x [in Hoare]
Himp.::x_';;'_x [in Equiv]
Himp.::x_';;'_x [in Hoare]
Himp.::'HAVOC'_x [in Hoare]
Himp.::'HAVOC'_x [in Equiv]
Himp.::'IFB'_x_'THEN'_x_'ELSE'_x_'FI' [in Equiv]
Himp.::'IFB'_x_'THEN'_x_'ELSE'_x_'FI' [in Hoare]
Himp.::'SKIP' [in Hoare]
Himp.::'SKIP' [in Equiv]
Himp.::'WHILE'_x_'DO'_x_'END' [in Hoare]
Himp.::'WHILE'_x_'DO'_x_'END' [in Equiv]

I

{{'_x_'}}'_x_'{{'_x_'}}'">If₁.:hoare_spec_scope:'{{'_x_'}}'_x_'{{'_x_'}}' [in Hoare]
If₁.::x_'/'_x_'\\'_x [in Hoare]
If₁.::x_'::='_x [in Hoare]
If₁.::x_';;'_x [in Hoare]
If₁.::'IFB'_x_'THEN'_x_'ELSE'_x_'FI' [in Hoare]
If₁.::'IF₁'_x_'THEN'_x_'FI' [in Hoare]
If₁.::'SKIP' [in Hoare]
If₁.::'WHILE'_x_'DO'_x_'END' [in Hoare]

L

LeModule.::x_'<='_x [in IndProp]
Loop.::x_'/'_x_'/'_x_'/'_x_'\\'_x_'#'_x [in PE]
Loop.::x_'/'_x_'\\'_x_'#'_x [in PE]
Loop.::x_'/'_x_'\\'_x_'/'_x_'/'_x [in PE]

M

MyEquality.:type_scope:x_'='_x [in ProofObjects]
MyIff.:type_scope:x_'<->'_x [in Logic]
MyNot.:type_scope:'~'_x [in Logic]

N

NatList.::x_'++'_x [in Lists]
NatList.::x_'::'_x [in Lists]
NatList.::'('_x_','_x_')' [in Lists]
NatList.::'['_x_';'_'..'_';'_x_']' [in Lists]
NatList.::'['_']' [in Lists]

R

RepeatExercise.::x_'/'_x_'\\'_x [in Hoare]
RepeatExercise.::x_'::='_x [in Hoare]
RepeatExercise.::x_';;'_x [in Hoare]
RepeatExercise.::'IFB'_x_'THEN'_x_'ELSE'_x_'FI' [in Hoare]
RepeatExercise.::'REPEAT'_x_'UNTIL'_x_'END' [in Hoare]
RepeatExercise.::'SKIP' [in Hoare]
RepeatExercise.::'WHILE'_x_'DO'_x_'END' [in Hoare]
{{'_x_'}}'_x_'{{'_x_'}}'">RepeatExercise.::'{{'_x_'}}'_x_'{{'_x_'}}' [in Hoare]
Repeat.::x_'/'_x_'\\'_x [in Auto]
Repeat.::x_'::='_x [in Auto]
Repeat.::x_';'_x [in Auto]
Repeat.::'IFB'_x_'THEN'_x_'ELSE'_x_'FI' [in Auto]
Repeat.::'REPEAT'_x_'UNTIL'_x_'END' [in Auto]
Repeat.::'SKIP' [in Auto]
Repeat.::'WHILE'_x_'DO'_x_'END' [in Auto]

S

SimpleArith1.::x_'==>'_x [in Smallstep]
STLCExtendedRecords.::x_'==>'_x [in Records]
STLCExtendedRecords.::x_'==>*'_x [in Records]
STLCExtendedRecords.::x_'|-'_x_'∈'_x [in Records]
STLCExtendedRecords.::'['_x_':='_x_']'_x [in Records]
STLCExtended.::x_'==>'_x [in MoreStlc]
STLCExtended.::x_'==>*'_x [in MoreStlc]
STLCExtended.::x_'|-'_x_'∈'_x [in MoreStlc]
STLCExtended.::'['_x_':='_x_']'_x [in MoreStlc]
STLCRef.RefsAndNontermination.::x_'/'_x_'==>+'_x_'/'_x [in References]
STLCRef.::x_'/'_x_'==>'_x_'/'_x [in References]
STLCRef.::x_'/'_x_'==>*'_x_'/'_x [in References]
STLCRef.::x_';'_x_'|-'_x_'∈'_x [in References]
STLCRef.::'['_x_':='_x_']'_x [in References]
STLC.::x_'==>'_x [in Stlc]
STLC.::x_'==>*'_x [in Stlc]
STLC.::x_'|-'_x_'∈'_x [in Stlc]
STLC.::'['_x_':='_x_']'_x [in Stlc]

T

Temp1.::x_'==>'_x [in Smallstep]
Temp2.::x_'==>'_x [in Smallstep]
Temp3.::x_'==>'_x [in Smallstep]
Temp4.Temp5.::x_'==>'_x [in Smallstep]
Temp4.::x_'==>'_x [in Smallstep]

:

Module Index

A

aevalR_division [in Imp]
aevalR_extended [in Imp]
AExp [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 RecordSub]
Examples [in Sub]
ExamplesInstantiations [in UseTactics]
ExamplesLets [in UseTactics]
Examples2 [in Sub]
Examples2 [in RecordSub]
ExAssertions [in Hoare]
Exercises [in Poly]
Exercises.Church [in Poly]

G

GenExample [in UseTactics]

H

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

I

If₁ [in Hoare]
IntrovExamples [in UseTactics]
InvertsExamples [in UseTactics]

L

LeModule [in IndProp]
LibTacticsCompatibility [in LibTactics]
Loop [in PE]

M

MumbleGrumble [in Poly]
MyEquality [in ProofObjects]
MyIff [in Logic]
MyNot [in Logic]

N

NaryExamples [in UseTactics]
NatList [in Lists]

P

PartialMap [in Lists]
Playground1 [in Basics]
Playground2 [in Basics]
PreservationProgressReferences [in UseAuto]
PreservationProgressStlc [in UseAuto]
Props [in ProofObjects]
Props.And [in ProofObjects]
Props.Ex [in ProofObjects]
Props.Or [in ProofObjects]
Pumping [in IndProp]

R

R [in IndProp]
Repeat [in Auto]
RepeatExercise [in Hoare]
RingDemo [in UseAuto]

S

T

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

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]

S

skip_axiom [in LibTactics]

Library Index

A

Auto

B

Basics
Bib

E

Equiv
Extraction

H

Hoare
HoareAsLogic
Hoare2

I

Imp
ImpCEvalFun
ImpParser
IndPrinciples
IndProp
Induction

L

LibTactics
Lists
Logic

M

Maps
MoreStlc

N

Norm

P

PE
Poly
Postscript
Preface
ProofObjects

R

Records
RecordSub
References
Rel

S

Smallstep
Stlc
StlcProp
Sub
Symbols

T

Tactics
Typechecking
Types

U

UseAuto
UseTactics

Lemma Index

A

abs_arrow [in RecordSub]
abs_arrow [in Sub]
aequiv_example [in Equiv]
aeval_weakening [in Equiv]
AExp.aeval_iff_aevalR [in Imp]
AExp.aeval_iff_aevalR' [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]
all3_spec [in Induction]
All_In [in Logic]
always_loop_hoare [in Hoare]
andb3_exchange [in Basics]
andb_commutative [in Basics]
andb_commutative' [in Basics]
andb_commutative'' [in Basics]
andb_eq_orb [in Basics]
andb_false_r [in Induction]
andb_true_elim2 [in Basics]
andb_true_iff [in Logic]
and_assoc [in Logic]
and_commut [in Logic]
and_example2 [in Logic]
and_example2' [in Logic]
and_example2'' [in Logic]
and_example3 [in Logic]
and_intro [in Logic]
apply_empty [in Maps]
apply_iff_example [in Logic]
app_assoc [in Poly]
app_length [in Poly]
app_length_cons [in Tactics]
app_length_twice [in Tactics]
app_nil_r [in Poly]
assign_aequiv [in Equiv]
assign_removes [in PE]

B

bassn_eval_false [in HoareAsLogic]
bequiv_example [in Equiv]
beq_idP [in Maps]
beq_id_false_iff [in Maps]
beq_id_refl [in Lists]
beq_id_refl [in Maps]
beq_id_true [in Tactics]
beq_id_true_iff [in Maps]
beq_list_true_iff [in Logic]
beq_natP [in IndProp]
beq_nat_false_iff [in Logic]
beq_nat_refl [in Induction]
beq_nat_sym [in Tactics]
beq_nat_trans [in Tactics]
beq_nat_true [in Tactics]
beq_nat_true_iff [in Logic]
beq_nat_0_l [in Tactics]
bexp_eval_false [in Hoare]
bexp_eval_true [in Hoare]
bool_canonical [in Types]
bool_fn_applied_thrice [in Tactics]
BreakImp.break_ignore [in Imp]
BreakImp.ceval_deterministic [in Imp]
BreakImp.while_break_true [in Imp]
BreakImp.while_continue [in Imp]
BreakImp.while_stops_on_break [in Imp]

C

canonical_forms_of_arrow_types [in Sub]
canonical_forms_of_arrow_types [in RecordSub]
canonical_forms_of_Bool [in Sub]
CAss_congruence [in Equiv]
ceval_and_ceval_step_coincide [in ImpCEvalFun]
ceval_deterministic [in Auto]
ceval_deterministic [in Imp]
ceval_deterministic' [in Auto]
ceval_deterministic' [in ImpCEvalFun]
ceval_deterministic'' [in Auto]
ceval_deterministic''' [in Auto]
ceval_deterministic'''' [in Auto]
ceval_deterministic''''' [in Auto]
ceval_deterministic'_alt [in Auto]
ceval_extensionality [in PE]
ceval_step_more [in ImpCEvalFun]
ceval_step__ceval [in ImpCEvalFun]
ceval__ceval_step [in ImpCEvalFun]
CIf_congruence [in Equiv]
CImp.par_body_n [in Smallstep]
CImp.par_body_n__Sn [in Smallstep]
CImp.par_loop_any_X [in Smallstep]
cmin_minimal [in Equiv]
combine_odd_even_elim_even [in Logic]
combine_odd_even_elim_odd [in Logic]
combine_odd_even_intro [in Logic]
combine_split [in Tactics]
compiler_is_correct [in Smallstep]
congruence_demo_1 [in UseAuto]
congruence_demo_2 [in UseAuto]
congruence_demo_3 [in UseAuto]
congruence_demo_4 [in UseAuto]
context_invariance [in Sub]
context_invariance [in RecordSub]
context_invariance [in Norm]
contradiction_implies_anything [in Logic]
contrapositive [in Logic]
CSeq_congruence [in Equiv]
CWhile_congruence [in Equiv]
c3_c4_different [in Equiv]

D

dec_while_correct [in Hoare2]
demo_auto_absurd_1 [in UseAuto]
demo_auto_absurd_2 [in UseAuto]
demo_clears_all_and_clears_but [in LibTactics]
demo_false [in UseTactics]
demo_false [in UseAuto]
demo_false_arg [in UseTactics]
demo_hint_unfold_context_1 [in UseAuto]
demo_hint_unfold_context_2 [in UseAuto]
demo_hint_unfold_goal_1 [in UseAuto]
demo_hint_unfold_goal_2 [in UseAuto]
demo_tryfalse [in UseTactics]
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]
dist_exists_or [in Logic]
dist_not_exists [in Logic]
div_mod_dec_correct [in Hoare2]
double_induction [in Tactics]
double_injective [in Tactics]
double_injective_FAILED [in Tactics]
double_injective_take2 [in Tactics]
double_injective_take2_FAILED [in Tactics]
double_neg [in Logic]
double_plus [in Induction]
dpow2_down_correct [in Hoare2]
duplicate_subst [in Norm]
dup_lemma [in LibTactics]

E

empty_is_empty [in IndProp]
EqualityExamples.demo_applys_eq_1 [in UseTactics]
EqualityExamples.demo_applys_eq_2 [in UseTactics]
EqualityExamples.demo_applys_eq_3 [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_0 [in LibTactics]
equates_1 [in LibTactics]
equates_2 [in LibTactics]
equates_3 [in LibTactics]
equates_4 [in LibTactics]
equates_5 [in LibTactics]
equates_6 [in LibTactics]
evalF_eval [in Smallstep]
eval_assign [in PE]
eval__multistep [in Smallstep]
evenb_double [in Logic]
evenb_double_conv [in Logic]
evenb_minus2 [in IndProp]
evenb_S [in Induction]
even5_nonsense [in IndProp]
even_bool_prop [in Logic]
evSS_ev [in IndProp]
evSS_ev [in IndProp]
ev'_ev [in IndProp]
ev_double [in IndProp]
ev_even [in IndProp]
ev_even [in IndProp]
ev_even_iff [in IndProp]
ev_ev' [in IndPrinciples]
ev_ev__ev [in IndProp]
ev_minus2 [in IndProp]
ev_minus2 [in IndProp]
ev_minus2' [in IndProp]
ev_plus4 [in IndProp]
ev_plus4 [in ProofObjects]
ev_plus_plus [in IndProp]
ev_sum [in IndProp]
ev_4 [in IndProp]
ev_4 [in ProofObjects]
ev_4' [in ProofObjects]
ev_4' [in IndProp]
ev_4'' [in ProofObjects]
ev_8 [in ProofObjects]
ExamplesInstantiations.substitution_preserves_typing [in UseTactics]
ExamplesLets.demo_lets_underscore [in UseTactics]
ExamplesLets.demo_lets_1 [in UseTactics]
ExamplesLets.demo_lets_2 [in UseTactics]
ExamplesLets.demo_lets_3 [in UseTactics]
ExamplesLets.demo_lets_4 [in UseTactics]
ExamplesLets.demo_lets_5 [in UseTactics]
excluded_middle_irrefutable [in Logic]
Exercises.curry_uncurry [in Poly]
Exercises.fold_length_correct [in Poly]
Exercises.uncurry_curry [in Poly]
exists_example_2 [in Logic]
ex_falso_quodlibet [in Logic]

F

False_and_P_imp [in HoareAsLogic]
false_beq_id [in Maps]
filter_exercise [in Tactics]
filter_not_empty_In [in IndProp]
filter_not_empty_In' [in IndProp]
find_parity_correct [in Hoare2]
find_parity_correct' [in Hoare2]
fold_constants_aexp_sound [in Equiv]
fold_constants_bexp_sound [in Equiv]
fold_constants_com_sound [in Equiv]
forallb_true_iff [in Logic]
four_is_even [in Logic]
free_in_context [in Norm]
free_in_context [in Sub]
free_in_context [in RecordSub]
f_equal [in Tactics]

G

GenExample.substitution_preserves_typing [in UseTactics]

H

has_type__wf [in RecordSub]
Himp.hoare_havoc [in Hoare]
Himp.ptwice_cequiv_pcopy [in Equiv]
Himp.pXY_cequiv_pYX [in Equiv]
Himp.p1_may_diverge [in Equiv]
Himp.p1_p2_equiv [in Equiv]
Himp.p2_may_diverge [in Equiv]
Himp.p3_p4_inequiv [in Equiv]
Himp.p5_p6_equiv [in Equiv]
Himp2.hoare_havoc_weakest [in Hoare2]
hoare_asgn [in Hoare]
hoare_asgn_fwd [in Hoare]
hoare_asgn_fwd_exists [in Hoare]
hoare_asgn_weakest [in Hoare2]
hoare_consequence [in Hoare]
hoare_consequence_post [in Hoare]
hoare_consequence_pre [in Hoare]
hoare_if [in Hoare]
hoare_post_true [in Hoare]
hoare_pre_false [in Hoare]
hoare_proof_complete [in HoareAsLogic]
hoare_proof_sound [in HoareAsLogic]
hoare_seq [in Hoare]
hoare_skip [in Hoare]
hoare_while [in Hoare]
H_Consequence_post [in HoareAsLogic]
H_Consequence_pre [in HoareAsLogic]
H_Post_True_deriv [in HoareAsLogic]
H_Pre_False_deriv [in HoareAsLogic]

I

identity_assignment [in Equiv]
identity_fn_applied_twice [in Basics]
IFB_false [in Equiv]
IFB_true [in Equiv]
IFB_true_simple [in Equiv]
iff_intro_swap [in LibTactics]
iff_refl [in Logic]
iff_reflect [in IndProp]
iff_sym [in Logic]
iff_trans [in Equiv]
iff_trans [in Logic]
If₁.hoare_if1_good [in Hoare]
if_minus_correct [in Hoare2]
if_minus_plus [in Hoare]
if_minus_plus_correct [in Hoare2]
inbP [in PE]
induct_height_max2 [in LibTactics]
inequiv_exercise [in Equiv]
instantiation_domains_match [in Norm]
instantiation_drop [in Norm]
instantiation_env_closed [in Norm]
instantiation_R [in Norm]
IntrovExamples.ceval_deterministic [in UseTactics]
IntrovExamples.ceval_deterministic' [in UseTactics]
IntrovExamples.dist_exists_or [in UseTactics]
IntrovExamples.exists_impl [in UseTactics]
inversion_ex₁ [in Tactics]
inversion_ex₂ [in Tactics]
inversion_ex₄ [in Tactics]
inversion_ex₅ [in Tactics]
InvertsExamples.ceval_deterministic [in UseTactics]
InvertsExamples.ceval_deterministic' [in UseTactics]
InvertsExamples.skip_left [in UseTactics]
InvertsExamples.skip_left' [in UseTactics]
in_app_iff [in Logic]
In_map [in Logic]
In_map_iff [in Logic]
in_re_match [in IndProp]
in_split [in IndProp]
is_wp_example [in Hoare2]

L

leb_complete [in IndProp]
leb_correct [in IndProp]
leb_iff [in IndProp]
leb_refl [in Induction]
leb_true_trans [in IndProp]
LeModule.test_le₁ [in IndProp]
LeModule.test_le₂ [in IndProp]
LeModule.test_le₃ [in IndProp]
le_antisym [in Auto]
le_antisymmetric [in Rel]
le_not_a_partial_function [in Rel]
le_not_symmetric [in Rel]
le_order [in Rel]
le_plus_l [in IndProp]
le_reflexive [in Rel]
le_Sn_le [in Rel]
le_Sn_n [in Rel]
le_step [in Rel]
le_S_n [in Rel]
le_trans [in IndProp]
le_trans [in Rel]
lookup_field_in_value [in RecordSub]
Loop.ceval_count_complete [in PE]
Loop.ceval_count_sound [in PE]
Loop.pe_ceval_count_le [in PE]
Loop.pe_compare_nil_lookup [in PE]
Loop.pe_compare_nil_update [in PE]
Loop.pe_com_complete [in PE]
Loop.pe_com_correct [in PE]
Loop.pe_com_sound [in PE]
loop_never_stops [in Imp]
loop_unrolling [in Equiv]
ltac_database_provide [in LibTactics]
ltac_something_eq [in LibTactics]
ltac_something_hide [in LibTactics]
ltac_something_show [in LibTactics]
lt_S [in IndProp]
lt_trans [in Rel]
lt_trans' [in Rel]
lt_trans'' [in Rel]
l₁ [in Hoare2]
l₂ [in Hoare2]
l₃ [in Hoare2]
l₃' [in Hoare2]
l₄ [in Hoare2]

M

map_rev [in Poly]
minus_diag [in Induction]
MStar' [in IndProp]
MStar'' [in IndProp]
MStar1 [in IndProp]
msubst_abs [in Norm]
msubst_app [in Norm]
msubst_closed [in Norm]
msubst_preserves_typing [in Norm]
msubst_R [in Norm]
msubst_var [in Norm]
multistep_App2 [in Norm]
multistep_congr_1 [in Smallstep]
multistep_congr_2 [in Smallstep]
multistep_preserves_R [in Norm]
multistep_preserves_R' [in Norm]
multistep__eval [in Smallstep]
multi_R [in Smallstep]
multi_trans [in Smallstep]
mult_assoc [in Induction]
mult_comm [in Induction]
mult_eq_0 [in Logic]
mult_plus_distr_r [in Induction]
mult_S_1 [in Basics]
mult_0 [in Logic]
mult_0_l [in Basics]
mult_0_plus [in Basics]
mult_0_plus' [in Induction]
mult_0_r [in Induction]
mult_0_r' [in IndPrinciples]
mult_0_r'' [in IndPrinciples]
mult_0_3 [in Logic]
mult_1_l [in Induction]
MUnion' [in IndProp]
mupdate_drop [in Norm]
mupdate_lookup [in Norm]
MyEquality.four [in ProofObjects]
MyEquality.leibniz_equality [in ProofObjects]

N

O

omega_demo_1 [in UseAuto]
omega_demo_2 [in UseAuto]
omega_demo_3 [in UseAuto]
omega_demo_4 [in UseAuto]
one_not_even [in IndProp]
orb_true_iff [in Logic]
order_matters_1 [in UseAuto]
order_matters_2 [in UseAuto]
or_assoc [in Logic]
or_commut [in Logic]
or_distributes_over_and [in Logic]
or_example [in Logic]
or_intro [in Logic]
O_le_n [in IndProp]

P

R

rcd_types_match [in RecordSub]
reduce_to_zero_correct' [in Hoare2]
reflect_iff [in IndProp]
refl_aequiv [in Equiv]
refl_bequiv [in Equiv]
refl_cequiv [in Equiv]
reg_exp_of_list_spec [in IndProp]
RepeatExercise.ex1_repeat_works [in Hoare]
Repeat.ceval_deterministic [in Auto]
Repeat.ceval_deterministic' [in Auto]
restricted_excluded_middle [in Logic]
rev_app_distr [in Poly]
rev_exercise1 [in Tactics]
rev_involutive [in Poly]
re_not_empty_correct [in IndProp]
RingDemo.ring_demo [in UseAuto]
rsc_R [in Rel]
rsc_trans [in Rel]
rtc_rsc_coincide [in Rel]
R.R_equiv_fR [in IndProp]
R_halts [in Norm]
R_typable_empty [in Norm]

S

T

Temp1.value_not_same_as_normal_form [in Smallstep]
Temp2.value_not_same_as_normal_form [in Smallstep]
Temp3.value_not_same_as_normal_form [in Smallstep]
Temp4.step_deterministic [in Smallstep]
Temp4.strong_progress [in Smallstep]
test_multistep_1 [in Smallstep]
test_multistep_1' [in Smallstep]
test_multistep_2 [in Smallstep]
test_multistep_3 [in Smallstep]
test_multistep_4 [in Smallstep]
transitivity_bad_hint_1 [in UseAuto]
transitivity_workaround_1 [in UseAuto]
transitivity_workaround_2 [in UseAuto]
trans_aequiv [in Equiv]
trans_bequiv [in Equiv]
trans_cequiv [in Equiv]
trans_eq [in Tactics]
True_is_true [in Logic]
tr_rev_correct [in Logic]
two_loops_correct [in Hoare2]
typable_empty__closed [in Norm]
typing_inversion_abs [in Sub]
typing_inversion_abs [in RecordSub]
typing_inversion_app [in RecordSub]
typing_inversion_app [in Sub]
typing_inversion_false [in Sub]
typing_inversion_if [in Sub]
typing_inversion_proj [in RecordSub]
typing_inversion_rcons [in RecordSub]
typing_inversion_true [in Sub]
typing_inversion_unit [in Sub]
typing_inversion_var [in Sub]
typing_inversion_var [in RecordSub]
t_apply_empty [in Maps]
t_update_eq [in Maps]
t_update_neq [in Maps]
t_update_permute [in Maps]
t_update_same [in Maps]
t_update_shadow [in Maps]

U

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

V

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

W

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

Z

zero_nbeq_plus_1 [in Basics]
zero_nbeq_S [in Induction]
zero_not_one [in Logic]
zero_not_one' [in Logic]
zero_or_succ [in Logic]
zprop_preserving [in Equiv]

Constructor Index

A

B

BAnd [in Imp]
Baz1 [in Lists]
Baz2 [in Lists]
bempty [in IndPrinciples]
BEq [in Imp]
BFalse [in Imp]
BLe [in Imp]
bleaf [in IndPrinciples]
blue [in IndPrinciples]
BNot [in Imp]
body [in PE]
bool_cons [in Poly]
bool_nil [in Poly]
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_AndStep [in Smallstep]
BS_AndTrueFalse [in Smallstep]
BS_AndTrueStep [in Smallstep]
BS_AndTrueTrue [in Smallstep]
BS_Eq [in Smallstep]
BS_Eq₁ [in Smallstep]
BS_Eq₂ [in Smallstep]
BS_LtEq [in Smallstep]
BS_LtEq1 [in Smallstep]
BS_LtEq2 [in Smallstep]
BS_NotFalse [in Smallstep]
BS_NotStep [in Smallstep]
BS_NotTrue [in Smallstep]
BTrue [in Imp]
bv_false [in Types]
bv_true [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]
digit [in ImpParser]
done [in PE]

E

EmptySet [in IndProp]
EmptyStr [in IndProp]
entry [in PE]
ev'_sum [in IndProp]
ev'_0 [in IndProp]
ev'_2 [in IndProp]
ev_SS [in Hoare2]
ev_SS [in IndProp]
ev_0 [in IndProp]
ev_0 [in Hoare2]
E_Ass [in Imp]
E_Const [in Smallstep]
E_IfFalse [in Imp]
E_IfTrue [in Imp]
E_None [in PE]
E_Plus [in Smallstep]
E_Seq [in Imp]
E_Skip [in Imp]
E_Some [in PE]
E_WhileEnd [in Imp]
E_WhileLoop [in Imp]

F

false [in Basics]
friday [in Basics]

G

Goto [in PE]
green [in IndPrinciples]

H

Himp.CAsgn [in Hoare]
Himp.CAss [in Equiv]
Himp.CHavoc [in Equiv]
Himp.CHavoc [in Hoare]
Himp.CIf [in Hoare]
Himp.CIf [in Equiv]
Himp.CSeq [in Hoare]
Himp.CSeq [in Equiv]
Himp.CSkip [in Hoare]
Himp.CSkip [in Equiv]
Himp.CWhile [in Hoare]
Himp.CWhile [in Equiv]
Himp.E_Ass [in Hoare]
Himp.E_Ass [in Equiv]
Himp.E_Havoc [in Hoare]
Himp.E_IfFalse [in Hoare]
Himp.E_IfFalse [in Equiv]
Himp.E_IfTrue [in Equiv]
Himp.E_IfTrue [in Hoare]
Himp.E_Seq [in Equiv]
Himp.E_Seq [in Hoare]
Himp.E_Skip [in Equiv]
Himp.E_Skip [in Hoare]
Himp.E_WhileEnd [in Hoare]
Himp.E_WhileEnd [in Equiv]
Himp.E_WhileLoop [in Hoare]
Himp.E_WhileLoop [in Equiv]
H_Asgn [in HoareAsLogic]
H_Consequence [in HoareAsLogic]
H_If [in HoareAsLogic]
H_Seq [in HoareAsLogic]
H_Skip [in HoareAsLogic]
H_While [in HoareAsLogic]

I

Id [in Lists]
Id [in Maps]
If [in PE]
If₁.CAss [in Hoare]
If₁.CIf [in Hoare]
If₁.CIf1 [in Hoare]
If₁.CSeq [in Hoare]
If₁.CSkip [in Hoare]
If₁.CWhile [in Hoare]
If₁.E_Ass [in Hoare]
If₁.E_IfFalse [in Hoare]
If₁.E_IfTrue [in Hoare]
If₁.E_Seq [in Hoare]
If₁.E_Skip [in Hoare]
If₁.E_WhileEnd [in Hoare]
If₁.E_WhileLoop [in Hoare]

L

leaf [in IndPrinciples]
LeModule.le_n [in IndProp]
LeModule.le_S [in IndProp]
le_n [in IndPrinciples]
le_S [in IndPrinciples]
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'WhileEnd [in PE]
Loop.E'WhileLoop [in PE]
Loop.PE_AssDynamic [in PE]
Loop.PE_AssStatic [in PE]
Loop.pe_ceval_count_intro [in PE]
Loop.PE_If [in PE]
Loop.PE_IfFalse [in PE]
Loop.PE_IfTrue [in PE]
Loop.PE_Seq [in PE]
Loop.PE_Skip [in PE]
Loop.PE_While [in PE]
Loop.PE_WhileEnd [in PE]
Loop.PE_WhileFixed [in PE]
Loop.PE_WhileFixedEnd [in PE]
Loop.PE_WhileFixedLoop [in PE]
Loop.PE_WhileLoop [in PE]
ltac_database_token [in LibTactics]
ltac_mark [in LibTactics]
ltac_no_arg [in LibTactics]
ltac_wild [in LibTactics]
ltac_wilds [in LibTactics]

M

MApp [in IndProp]
MChar [in IndProp]
MEmpty [in IndProp]
monday [in Basics]
MStarApp [in IndProp]
MStar0 [in IndProp]
multi_refl [in Smallstep]
multi_step [in Smallstep]
MumbleGrumble.a [in Poly]
MumbleGrumble.b [in Poly]
MumbleGrumble.c [in Poly]
MumbleGrumble.d [in Poly]
MumbleGrumble.e [in Poly]
MUnionL [in IndProp]
MUnionR [in IndProp]
MyEquality.eq_refl [in ProofObjects]

N

NatList.cons [in Lists]
NatList.nil [in Lists]
NatList.None [in Lists]
NatList.pair [in Lists]
NatList.Some [in Lists]
nbranch [in IndPrinciples]
ncons [in IndPrinciples]
ne_1 [in IndProp]
ne_2 [in IndProp]
nil [in Poly]
nil' [in Poly]
nn [in IndProp]
nnil [in IndPrinciples]
nnil1 [in IndPrinciples]
no [in IndPrinciples]
node [in IndPrinciples]
None [in Poly]
NoneE [in ImpParser]
nsnoc1 [in IndPrinciples]
nv_succ [in Types]
nv_zero [in Types]

O

other [in ImpParser]

P

P [in Smallstep]
pair [in Poly]
PartialMap.empty [in Lists]
PartialMap.record [in Lists]
PE_AssDynamic [in PE]
PE_AssStatic [in PE]
pe_ceval_intro [in PE]
PE_If [in PE]
PE_IfFalse [in PE]
PE_IfTrue [in PE]
pe_peval_intro [in PE]
PE_Seq [in PE]
PE_Skip [in PE]
Playground1.O [in Basics]
Playground1.S [in Basics]
Props.And.conj [in ProofObjects]
Props.Ex.ex_intro [in ProofObjects]
Props.I [in ProofObjects]
Props.Or.or_introl [in ProofObjects]
Props.Or.or_intror [in ProofObjects]

R

S

T

U

Union [in IndProp]

V

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

W

wednesday [in Basics]
wfTArrow [in RecordSub]
wfTBase [in RecordSub]
wfTRCons [in RecordSub]
wfTRNil [in RecordSub]
wfTTop [in RecordSub]
white [in ImpParser]
wrong_ev_SS [in IndProp]
wrong_ev_0 [in IndProp]

Y

yes [in IndPrinciples]

Axiom Index

E

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

F

functional_extensionality [in Logic]

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_refl [in UseAuto]
subtype_trans [in UseAuto]

T

typ [in UseAuto]

Inductive Index

A

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

B

baz [in Lists]
bexp [in Imp]
block [in PE]
bool [in Basics]
boollist [in Poly]
Boxer [in LibTactics]
BreakImp.ceval [in Imp]
BreakImp.com [in Imp]
BreakImp.status [in Imp]
bstep [in Smallstep]
bvalue [in Types]
byntree [in IndPrinciples]

C

ceval [in Imp]
chartype [in ImpParser]
CImp.com [in Smallstep]
CImp.cstep [in Smallstep]
clos_refl_trans [in Rel]
clos_refl_trans_1n [in Rel]
com [in Imp]
Combined.step [in Smallstep]
Combined.tm [in Smallstep]
Combined.value [in Smallstep]
cstep [in Smallstep]

D

day [in Basics]
dcom [in Hoare2]

E

ev [in IndProp]
ev [in Hoare2]
eval [in Smallstep]
ev' [in IndProp]
exp_match [in IndProp]
ExSet [in IndPrinciples]

F

foo' [in IndPrinciples]

H

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

I

id [in Lists]
id [in Maps]
If₁.ceval [in Hoare]
If₁.com [in Hoare]
instantiation [in Norm]

L

le [in IndPrinciples]
LeModule.le [in IndProp]
list [in Poly]
list' [in Poly]
Loop.ceval_count [in PE]
Loop.pe_ceval_count [in PE]
Loop.pe_com [in PE]
Ltac_database_token [in LibTactics]
ltac_Mark [in LibTactics]
ltac_No_arg [in LibTactics]
ltac_Wild [in LibTactics]
ltac_Wilds [in LibTactics]

M

multi [in Smallstep]
MumbleGrumble.grumble [in Poly]
MumbleGrumble.mumble [in Poly]
MyEquality.eq [in ProofObjects]

N

natlist [in IndPrinciples]
NatList.natlist [in Lists]
NatList.natoption [in Lists]
NatList.natprod [in Lists]
natlist1 [in IndPrinciples]
next_even [in IndProp]
next_nat [in IndProp]
nostutter [in IndProp]
no_whilesR [in Imp]
nvalue [in Types]

O

option [in Poly]
optionE [in ImpParser]

P

parity_label [in PE]
PartialMap.partial_map [in Lists]
peval [in PE]
pe_ceval [in PE]
pe_com [in PE]
pe_peval [in PE]
Playground1.nat [in Basics]
prod [in Poly]
Props.And.and [in ProofObjects]
Props.Ex.ex [in ProofObjects]
Props.False [in ProofObjects]
Props.Or.or [in ProofObjects]
Props.True [in ProofObjects]

R

record_tm [in RecordSub]
record_ty [in RecordSub]
reflect [in IndProp]
reg_exp [in IndProp]
RepeatExercise.ceval [in Hoare]
RepeatExercise.com [in Hoare]
repeats [in IndProp]
Repeat.ceval [in Auto]
Repeat.com [in Auto]
rgb [in IndPrinciples]
R.R [in IndProp]

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 Norm]
tm [in Types]
tm [in RecordSub]
tm [in Sub]
tm [in Smallstep]
tree [in IndPrinciples]
ty [in Types]
ty [in RecordSub]
ty [in Sub]
ty [in Norm]

V

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

W

well_formed_ty [in RecordSub]
wrong_ev [in IndProp]

Y

yesno [in IndPrinciples]

Section Index

D

DemoAbsurd1 [in UseAuto]

E

equatesLemma [in LibTactics]

H

HintsTransitivity [in UseAuto]

Abbreviation Index

E

Examples.A [in RecordSub]
Examples.A [in Sub]
Examples.B [in Sub]
Examples.B [in RecordSub]
Examples.C [in RecordSub]
Examples.C [in Sub]
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

B

bar [in Tactics]
bassn [in Hoare]
bequiv [in Equiv]
beq_id [in Maps]
beq_id [in Lists]
beq_list [in Logic]
beq_nat [in Basics]
beval [in Imp]
bexp1 [in Imp]
bignumber [in ImpParser]
blt_nat [in Basics]
btrans_sound [in Equiv]
build_symtable [in ImpParser]

C

capprox [in Equiv]
cequiv [in Equiv]
ceval_example1 [in Imp]
ceval_example2 [in Imp]
ceval_fun_no_while [in Imp]
ceval_step [in ImpCEvalFun]
ceval_step1 [in ImpCEvalFun]
ceval_step2 [in ImpCEvalFun]
ceval_step3 [in ImpCEvalFun]
CImp.cmultistep [in Smallstep]
CImp.par_loop [in Smallstep]
CImp.par_loop_example_0 [in Smallstep]
CImp.par_loop_example_2 [in Smallstep]
classifyChar [in ImpParser]
closed [in Norm]
closed_env [in Norm]
cmin [in Equiv]
COIND [in LibTactics]
combine [in Poly]
combine_odd_even [in Logic]
compiler_is_correct_statement [in Smallstep]
congruence_example [in Equiv]
constfun [in Poly]
constfun_example1 [in Poly]
constfun_example2 [in Poly]
context [in Sub]
context [in Norm]
context [in RecordSub]
countoddmembers' [in Poly]
ctrans_sound [in Equiv]
c₃ [in Equiv]
c₄ [in Equiv]

D

dec_correct [in Hoare2]
dec_while [in Hoare2]
deterministic [in Smallstep]
de_morgan_not_and_not [in Logic]
div_mod_dec [in Hoare2]
doit3times [in Poly]
double [in Induction]
double_negation_elimination [in Logic]
dpow2_down [in Hoare2]
drop [in Norm]

E

F

factorial [in Basics]
fact_in_coq [in Imp]
filter [in Poly]
filter_even_gt₇ [in Poly]
find_parity [in Hoare2]
find_parity_dec [in Hoare2]
find_parity_dec' [in Hoare2]
firstExpect [in ImpParser]
flat_map [in Poly]
fold [in Poly]
fold_aexp_ex₁ [in Equiv]
fold_aexp_ex₂ [in Equiv]
fold_bexp_ex₁ [in Equiv]
fold_bexp_ex₂ [in Equiv]
fold_com_ex₁ [in Equiv]
fold_constants_aexp [in Equiv]
fold_constants_bexp [in Equiv]
fold_constants_com [in Equiv]
fold_example1 [in Poly]
fold_example2 [in Poly]
fold_example3 [in Poly]
foo [in Tactics]
forallb [in Logic]
fst [in Poly]
ftrue [in Poly]
function_equality_ex [in Logic]

H

halts [in Norm]
has_type_not [in Types]
has_type_1 [in Types]
hd_error [in Poly]
Himp.cequiv [in Equiv]
Himp.havoc_example1 [in Equiv]
Himp.havoc_example2 [in Equiv]
Himp.havoc_pre [in Hoare]
Himp.hoare_triple [in Hoare]
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]
hoare_asgn_example1 [in Hoare]
hoare_asgn_example1' [in Hoare]
hoare_asgn_example3 [in Hoare]
hoare_asgn_example4 [in Hoare]
hoare_triple [in Hoare]

I

If₁.hoare_triple [in Hoare]
if_example [in Hoare]
if_minus_dec [in Hoare2]
if_minus_plus_com [in Hoare2]
if_minus_plus_dec [in Hoare2]
implies_to_or [in Logic]
In [in Logic]
inb [in PE]
injective [in Logic]
inversion_ex₃ [in Tactics]
inversion_ex₆ [in Tactics]
InvertsExamples.typing_nonexample_1 [in UseTactics]
In_example_1 [in Logic]
In_example_2 [in Logic]
isAlpha [in ImpParser]
isDigit [in ImpParser]
isLowerAlpha [in ImpParser]
isWhite [in ImpParser]
is_even_prime [in Logic]
is_fortytwo [in Auto]
is_three [in Logic]
is_wp [in Hoare2]

K

keval [in PE]
keval_example [in PE]

L

leb [in Basics]
lemma_application_ex [in Logic]
length [in Poly]
length_is_1 [in Poly]
list123 [in Poly]
list123' [in Poly]
list123'' [in Poly]
list123''' [in Poly]
list_of_string [in ImpParser]
lookup [in Norm]
loop [in Imp]
Loop.pe_loop_example1 [in PE]
Loop.pe_loop_example2 [in PE]
Loop.pe_loop_example3 [in PE]
Loop.pe_loop_example4 [in PE]
Loop.square_loop [in PE]
lt [in IndProp]
ltac_database [in LibTactics]
ltac_nat_from_int [in LibTactics]
ltac_something [in LibTactics]
ltac_tag_subst [in LibTactics]
ltac_to_generalize [in LibTactics]

M

many [in ImpParser]
many_helper [in ImpParser]
map [in Poly]
minustwo [in Basics]
msubst [in Norm]
multistep [in Types]
mupdate [in Norm]
MyEquality.four' [in ProofObjects]
MyEquality.singleton [in ProofObjects]
myFact [in UseAuto]
MyIff.iff [in Logic]
mynil [in Poly]
mynil [in Poly]
mynil' [in Poly]
MyNot.not [in Logic]

N

O

oddb [in Basics]
option_map [in Poly]
orb [in Basics]
order [in Rel]

P

parity [in PE]
parity [in Hoare2]
parity_body [in PE]
parity_dec [in Hoare2]
parity_eval [in PE]
parse [in ImpParser]
parseAExp [in ImpParser]
parseAtomicExp [in ImpParser]
parseBExp [in ImpParser]
parseConjunctionExp [in ImpParser]
parseIdentifier [in ImpParser]
parseNumber [in ImpParser]
parsePrimaryExp [in ImpParser]
parseProductExp [in ImpParser]
parser [in ImpParser]
parseSequencedCommand [in ImpParser]
parseSimpleCommand [in ImpParser]
parseSumExp [in ImpParser]
PartialMap.find [in Lists]
PartialMap.update [in Lists]
partial_function [in Rel]
partial_map [in Maps]
partition [in Poly]
peirce [in Logic]
pe_add [in PE]
pe_aexp [in PE]
pe_bexp [in PE]
pe_block [in PE]
pe_block_example [in PE]
pe_compare [in PE]
pe_consistent [in PE]
pe_disagree_at [in PE]
pe_example1 [in PE]
pe_example2 [in PE]
pe_example3 [in PE]
pe_lookup [in PE]
pe_program [in PE]
pe_remove [in PE]
pe_removes [in PE]
pe_state [in PE]
pe_unique [in PE]
pe_update [in PE]
Playground1.pred [in Basics]
Playground2.minus [in Basics]
Playground2.mult [in Basics]
Playground2.plus [in Basics]
Playground2.test_mult1 [in Basics]
plus' [in Basics]
plus2 [in Imp]
plus3 [in Poly]
plus_fact [in Logic]
post [in Hoare2]
pow2 [in Hoare2]
pre [in Hoare2]
preorder [in Rel]
prog [in Smallstep]
program [in PE]
prog_a [in Equiv]
prog_b [in Equiv]
prog_c [in Equiv]
prog_d [in Equiv]
prog_e [in Equiv]
prog_f [in Equiv]
prog_g [in Equiv]
prog_h [in Equiv]
prog_i [in Equiv]
Props.and_comm' [in ProofObjects]
Props.and_comm'_aux [in ProofObjects]
Props.conj_fact [in ProofObjects]
Props.ex_ev_Sn [in ProofObjects]
Props.or_comm [in ProofObjects]
Props.some_nat_is_even [in ProofObjects]
Pumping.napp [in IndProp]
Pumping.pumping_constant [in IndProp]
pup_to_n [in Imp]
pup_to_n [in ImpCEvalFun]
P_m0r [in IndPrinciples]
P_m0r' [in IndPrinciples]

Q

quiz6 [in ProofObjects]

R

R [in Norm]
real_fact [in Hoare2]
reduce_to_zero' [in Hoare2]
reflexive [in Rel]
reg_exp_ex₁ [in IndProp]
reg_exp_ex₂ [in IndProp]
reg_exp_ex₃ [in IndProp]
reg_exp_ex₄ [in IndProp]
reg_exp_of_list [in IndProp]
relation [in Rel]
relation [in Smallstep]
repeat [in Poly]
RepeatExercise.ex1_repeat [in Hoare]
RepeatExercise.hoare_triple [in Hoare]
repeat' [in Poly]
repeat'' [in Poly]
repeat''' [in Poly]
rev [in Poly]
rev_append [in Logic]
re_chars [in IndProp]
re_not_empty [in IndProp]
rm [in LibTactics]
R.fR [in IndProp]

S

T

tass [in Norm]
Temp4.bool_step_prop1 [in Smallstep]
Temp4.bool_step_prop2 [in Smallstep]
Temp4.bool_step_prop3 [in Smallstep]
Temp4.Temp5.bool_step_prop4 [in Smallstep]
Temp4.Temp5.bool_step_prop4_holds [in Smallstep]
testParsing [in ImpParser]
test_andb31 [in Basics]
test_andb32 [in Basics]
test_andb33 [in Basics]
test_andb34 [in Basics]
test_anon_fun' [in Poly]
test_blt_nat1 [in Basics]
test_blt_nat2 [in Basics]
test_blt_nat3 [in Basics]
test_ceval [in ImpCEvalFun]
test_countoddmembers'1 [in Poly]
test_countoddmembers'2 [in Poly]
test_countoddmembers'3 [in Poly]
test_doit3times [in Poly]
test_doit3times' [in Poly]
test_factorial1 [in Basics]
test_factorial2 [in Basics]
test_filter1 [in Poly]
test_filter2 [in Poly]
test_filter2' [in Poly]
test_filter_even_gt7_1 [in Poly]
test_filter_even_gt7_2 [in Poly]
test_flat_map1 [in Poly]
test_hd_error1 [in Poly]
test_hd_error2 [in Poly]
test_leb1 [in Basics]
test_leb2 [in Basics]
test_leb3 [in Basics]
test_length1 [in Poly]
test_map1 [in Poly]
test_map2 [in Poly]
test_map3 [in Poly]
test_nandb1 [in Basics]
test_nandb2 [in Basics]
test_nandb3 [in Basics]
test_nandb4 [in Basics]
test_next_weekday [in Basics]
test_nostutter_1 [in IndProp]
test_nostutter_2 [in IndProp]
test_nostutter_3 [in IndProp]
test_nostutter_4 [in IndProp]
test_nth_error1 [in Poly]
test_nth_error2 [in Poly]
test_nth_error3 [in Poly]
test_oddb1 [in Basics]
test_oddb2 [in Basics]
test_orb1 [in Basics]
test_orb2 [in Basics]
test_orb3 [in Basics]
test_orb4 [in Basics]
test_orb5 [in Basics]
test_partition1 [in Poly]
test_partition2 [in Poly]
test_pe_aexp1 [in PE]
test_pe_bexp1 [in PE]
test_pe_bexp2 [in PE]
test_pe_update [in PE]
test_plus3 [in Poly]
test_plus3' [in Poly]
test_plus3'' [in Poly]
test_repeat1 [in Poly]
test_repeat2 [in Poly]
test_rev1 [in Poly]
test_rev2 [in Poly]
test_split [in Poly]
text_pe_aexp2 [in PE]
tlookup [in RecordSub]
Tlookup [in RecordSub]
token [in ImpParser]
tokenize [in ImpParser]
tokenize_ex₁ [in ImpParser]
tokenize_helper [in ImpParser]
total_map [in Maps]
transitive [in Rel]
trans_eq_example [in Tactics]
trans_eq_example' [in Tactics]
trans_eq_exercise [in Tactics]
tr_rev [in Logic]
two_loops_dec [in Hoare2]
t_empty [in Maps]
t_update [in Maps]

U

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

V

value [in Types]
verification_conditions [in Hoare2]

W

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

(2854 entries)

Notation Index

(174 entries)

Module Index

(82 entries)

Variable Index

(8 entries)

Library Index

(39 entries)

Lemma Index

(768 entries)

Constructor Index

(854 entries)

Axiom Index

(12 entries)

Inductive Index

(184 entries)

Section Index

(3 entries)

Abbreviation Index

(55 entries)

Definition Index

(675 entries)