Global Index

other

(2764 entries)

Notation Index

other

(188 entries)

Module Index

other

(71 entries)

Variable Index

other

(8 entries)

Library Index

other

(39 entries)

Lemma Index

other

(741 entries)

Constructor Index

other

(848 entries)

Axiom Index

other

(12 entries)

Inductive Index

other

(187 entries)

Section Index

other

(4 entries)

Abbreviation Index

other

(55 entries)

Definition Index

other

(611 entries)

Global Index

A

abs_arrow [lemma, in Sub]
abs_arrow [lemma, in RecordSub]
add1 [definition, in ProofObjects]
admit [definition, in Basics]
admit [definition, in SfLib]
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.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.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.ev100 [lemma, in Imp]
AExp.ev100' [lemma, 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.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_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_if2 [constructor, in Norm]
afi_if1 [constructor, in Norm]
afi_if0 [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_if3 [constructor, in Sub]
afi_if2 [constructor, in Sub]
afi_if1 [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]
ai_later [constructor, in MoreLogic]
ai_here [constructor, in MoreLogic]
ai_later [constructor, in SfLib]
ai_here [constructor, in SfLib]
all [inductive, in MoreLogic]
all3_spec [lemma, in Induction]
alpha [constructor, in ImpParser]
always_loop_hoare [lemma, in Hoare]
AMinus [constructor, in Imp]
AMult [constructor, in Imp]
amultistep [definition, in Types]
and [inductive, in Logic]
andb [definition, in Basics]
andb_eq_orb [lemma, in Basics]
andb_false [lemma, in Logic]
andb_true_intro [lemma, in Logic]
andb_prop [lemma, in Logic]
andb_false_r [lemma, in Induction]
andb_true_elim2 [lemma, in Induction]
andb_true_elim1 [lemma, in Induction]
andb_true [lemma, in SfLib]
andb_true_elim2 [lemma, in SfLib]
andb_true_elim1 [lemma, in SfLib]
andb3 [definition, in Basics]
and_commut [lemma, in ProofObjects]
and_example [lemma, in ProofObjects]
and_assoc [lemma, in Logic]
and_commut [lemma, in Logic]
and_example' [lemma, in Logic]
and_example [lemma, in Logic]
antisymmetric [definition, in Rel]
ANum [constructor, in Imp]
APlus [constructor, in Imp]
app [definition, in Poly]
appears_in_app_split [lemma, in MoreLogic]
appears_in_app [lemma, in MoreLogic]
appears_in [inductive, in MoreLogic]
appears_free_in [inductive, in Norm]
appears_free_in [inductive, in Sub]
appears_in [inductive, in SfLib]
appears_free_in [inductive, in RecordSub]
app_length [lemma, in MoreLogic]
app_appears_in [lemma, in MoreLogic]
app_length_twice [lemma, in MoreCoq]
app_length_cons [lemma, in MoreCoq]
app' [definition, in Poly]
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_example [definition, in Hoare]
assn_sub [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_Mult2 [constructor, in Smallstep]
AS_Mult1 [constructor, in Smallstep]
AS_Mult [constructor, in Smallstep]
AS_Minus2 [constructor, in Smallstep]
AS_Minus1 [constructor, in Smallstep]
AS_Minus [constructor, in Smallstep]
AS_Plus2 [constructor, in Smallstep]
AS_Plus1 [constructor, in Smallstep]
AS_Plus [constructor, in Smallstep]
AS_Id [constructor, in Smallstep]
atrans_sound [definition, in Equiv]
Auto [library]
auto_example_8' [definition, in Auto]
auto_example_8 [definition, in Auto]
auto_example_7' [definition, in Auto]
auto_example_7 [definition, in Auto]
auto_example_6' [definition, in Auto]
auto_example_6 [definition, in Auto]
auto_example_5 [definition, in Auto]
auto_example_4 [definition, in Auto]
auto_example_3 [definition, in Auto]
auto_example_2 [definition, in Auto]
auto_example_1' [definition, in Auto]
auto_example_1 [definition, in Auto]
aval [inductive, in Smallstep]
av_num [constructor, in Smallstep]

B

BAnd [constructor, in Imp]
Basics [library]
bassn [definition, in Hoare]
bassn_eval_false [lemma, in HoareAsLogic]
beatiful_plus3'' [definition, in ProofObjects]
beautiful [inductive, in Prop]
beautiful_iff_gorgeous [definition, in ProofObjects]
beautiful_plus3' [definition, in ProofObjects]
beautiful_plus3 [definition, in ProofObjects]
beautiful__gorgeous [lemma, in Prop]
beautiful_plus_eight [lemma, in Prop]
bempty [constructor, in MoreInd]
BEq [constructor, in Imp]
bequiv [definition, in Equiv]
bequiv_example [lemma, in Equiv]
beq_nat [definition, in Basics]
beq_nat_false [lemma, in Logic]
beq_nat_refl [lemma, in Induction]
beq_nat_trans [lemma, in MoreCoq]
beq_nat_sym [lemma, in MoreCoq]
beq_nat_true [lemma, in MoreCoq]
beq_nat_0_r [lemma, in MoreCoq]
beq_nat_0_l [lemma, in MoreCoq]
beq_nat_sym [lemma, in SfLib]
between [definition, in Prop]
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]
bignumber [definition, in ImpParser]
BLe [constructor, in Imp]
bleaf [constructor, in MoreInd]
ble_nat [definition, in Basics]
ble_nat_refl [lemma, in Induction]
ble_nat_false [lemma, in SfLib]
ble_nat_true [lemma, in SfLib]
ble_nat [definition, in SfLib]
ble_nat_false_iff [lemma, in Hoare2]
ble_nat_true_iff [lemma, in Hoare2]
ble_nat_false [lemma, in Prop]
ble_nat_true_trans [lemma, in Prop]
ble_nat_true [lemma, in Prop]
block [inductive, in PE]
blt_nat [definition, in Basics]
blue [constructor, in MoreInd]
BNot [constructor, in Imp]
body [constructor, in PE]
bool [inductive, in Basics]
boollist [inductive, in Poly]
bool_cons [constructor, in Poly]
bool_nil [constructor, in Poly]
bool_fn_applied_thrice [lemma, in MoreCoq]
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.SBreak [constructor, in Imp]
BreakImp.SContinue [constructor, in Imp]
BreakImp.status [inductive, 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]
IFB _ THEN _ ELSE _ FI [notation, in Imp]
SKIP [notation, in Imp]
WHILE _ DO _ END [notation, in Imp]
bstep [inductive, in Smallstep]
BS_AndStep [constructor, in Smallstep]
BS_AndTrueStep [constructor, in Smallstep]
BS_AndFalse [constructor, in Smallstep]
BS_AndTrueFalse [constructor, in Smallstep]
BS_AndTrueTrue [constructor, in Smallstep]
BS_NotStep [constructor, in Smallstep]
BS_NotFalse [constructor, in Smallstep]
BS_NotTrue [constructor, in Smallstep]
BS_LtEq2 [constructor, in Smallstep]
BS_LtEq1 [constructor, in Smallstep]
BS_LtEq [constructor, in Smallstep]
BS_Eq2 [constructor, in Smallstep]
BS_Eq1 [constructor, in Smallstep]
BS_Eq [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 MoreInd]
b_times2' [definition, in ProofObjects]
b_plus3'' [definition, in ProofObjects]
b_plus3' [definition, in ProofObjects]
b_plus3 [lemma, in ProofObjects]
b_timesm [lemma, in Prop]
b_times2 [lemma, in Prop]
b_sum [constructor, in Prop]
b_5 [constructor, in Prop]
b_3 [constructor, in Prop]
b_0 [constructor, in Prop]

C

D

day [inductive, in Basics]
DCAsgn [constructor, in Hoare2]
DCIf [constructor, in Hoare2]
dcom [inductive, in Hoare2]
DCPost [constructor, in Hoare2]
DCPre [constructor, in Hoare2]
DCSeq [constructor, in Hoare2]
DCSkip [constructor, in Hoare2]
DCWhile [constructor, in Hoare2]
dec_while_correct [lemma, in Hoare2]
dec_correct [definition, in Hoare2]
dec_while [definition, in Hoare2]
DemoAbsurd1 [section, in UseAuto]
demo_tryfalse [lemma, in UseTactics]
demo_false_arg [lemma, in UseTactics]
demo_false [lemma, in UseTactics]
demo_false [lemma, in UseAuto]
demo_auto_absurd_2 [lemma, in UseAuto]
demo_auto_absurd_1 [lemma, in UseAuto]
demo_hint_unfold_context_2 [lemma, in UseAuto]
demo_hint_unfold_context_1 [lemma, in UseAuto]
demo_hint_unfold_goal_2 [lemma, in UseAuto]
demo_hint_unfold_goal_1 [lemma, in UseAuto]
deterministic [definition, in SfLib]
DeterministicImp [module, in UseAuto]
DeterministicImp.ceval_deterministic'''' [lemma, in UseAuto]
DeterministicImp.ceval_deterministic''' [lemma, in UseAuto]
DeterministicImp.ceval_deterministic'' [lemma, in UseAuto]
DeterministicImp.ceval_deterministic' [lemma, in UseAuto]
DeterministicImp.ceval_deterministic [lemma, in UseAuto]
de_morgan_not_and_not [definition, in Logic]
digit [constructor, in ImpParser]
dist_exists_or [lemma, in MoreLogic]
dist_not_exists [lemma, in MoreLogic]
doit3times [definition, in Poly]
done [constructor, in PE]
double [definition, in Induction]
double_neg [lemma, in Logic]
double_plus [lemma, in Induction]
double_induction [lemma, in MoreCoq]
double_injective_take2 [lemma, in MoreCoq]
double_injective_take2_FAILED [lemma, in MoreCoq]
double_injective [lemma, in MoreCoq]
double_injective_FAILED [lemma, in MoreCoq]
double_even [lemma, in Prop]
drop [definition, in Norm]
duplicate_subst [lemma, in Norm]
dup_lemma [lemma, in LibTactics]

E

eight_is_beautiful''' [definition, in ProofObjects]
eight_is_beautiful'' [lemma, in ProofObjects]
eight_is_beautiful' [lemma, in ProofObjects]
eight_is_beautiful [lemma, in ProofObjects]
eight_is_beautiful [lemma, in Prop]
empty [definition, in Sub]
empty [definition, in SfLib]
empty [definition, in RecordSub]
empty_state [definition, in Imp]
empty_relation [inductive, in SfLib]
empty_pe_state [definition, in PE]
entry [constructor, in PE]
env [definition, in Norm]
EqualityExamples [module, in UseTactics]
EqualityExamples.big_expression_using [axiom, in UseTactics]
EqualityExamples.demo_applys_eq_3 [lemma, in UseTactics]
EqualityExamples.demo_applys_eq_2 [lemma, in UseTactics]
EqualityExamples.demo_applys_eq_1 [lemma, in UseTactics]
EqualityExamples.demo_fequals [lemma, in UseTactics]
EqualityExamples.demo_substs [lemma, in UseTactics]
EqualityExamples.mult_0_plus'' [lemma, in UseTactics]
EqualityExamples.mult_0_plus' [lemma, in UseTactics]
EqualityExamples.mult_0_plus [lemma, in UseTactics]
equality_by_auto [lemma, in UseAuto]
equatesLemma [section, in LibTactics]
equatesLemma.A0 [variable, in LibTactics]
equatesLemma.A1 [variable, in LibTactics]
equatesLemma.A2 [variable, in LibTactics]
equatesLemma.A3 [variable, in LibTactics]
equatesLemma.A4 [variable, in LibTactics]
equatesLemma.A5 [variable, in LibTactics]
equatesLemma.A6 [variable, in LibTactics]
equates_6 [lemma, in LibTactics]
equates_5 [lemma, in LibTactics]
equates_4 [lemma, in LibTactics]
equates_3 [lemma, in LibTactics]
equates_2 [lemma, in LibTactics]
equates_1 [lemma, in LibTactics]
equates_0 [lemma, in LibTactics]
Equiv [library]
equivalence [definition, in Rel]
eq_nat_dec [lemma, in MoreLogic]
eq_add_S [lemma, in MoreCoq]
eq_id [lemma, in SfLib]
eq_id_dec [lemma, in SfLib]
eq' [inductive, in MoreInd]
eq' [definition, in LibTactics]
ev [inductive, in SfLib]
ev [inductive, in Prop]
eval [inductive, in Smallstep]
evalF [definition, in Smallstep]
evalF_eval [lemma, in Smallstep]
eval__multistep [lemma, in Smallstep]
eval_assign [lemma, in PE]
even [definition, in Prop]
evenb [definition, in Basics]
evenb_n__oddb_Sn [lemma, in Induction]
even__ev' [lemma, in MoreInd]
even5_nonsense [lemma, in Prop]
ev_not_ev_S [lemma, in SfLib]
ev_SS [constructor, in SfLib]
ev_0 [constructor, in SfLib]
ev_plus_plus [lemma, in Prop]
ev_ev__ev [lemma, in Prop]
ev_minus2 [lemma, in Prop]
ev_sum [lemma, in Prop]
ev__even [lemma, in Prop]
ev_SS [constructor, in Prop]
ev_0 [constructor, in Prop]
ex [inductive, in MoreLogic]
Examples [module, in Sub]
Examples [module, in RecordSub]
ExamplesInstantiations [module, in UseTactics]
ExamplesInstantiations.substitution_preserves_typing [lemma, in UseTactics]
ExamplesLets [module, in UseTactics]
ExamplesLets.demo_lets_underscore [lemma, in UseTactics]
ExamplesLets.demo_lets_5 [lemma, in UseTactics]
ExamplesLets.demo_lets_4 [lemma, in UseTactics]
ExamplesLets.demo_lets_3 [lemma, in UseTactics]
ExamplesLets.demo_lets_2 [lemma, in UseTactics]
ExamplesLets.demo_lets_1 [lemma, in UseTactics]
ExamplesLets.typing_inversion_var [axiom, in UseTactics]
Examples.A [abbreviation, in Sub]
Examples.A [abbreviation, in RecordSub]
Examples.B [abbreviation, in Sub]
Examples.B [abbreviation, in RecordSub]
Examples.C [abbreviation, in Sub]
Examples.C [abbreviation, in RecordSub]
Examples.Employee [definition, in Sub]
Examples.Float [abbreviation, in Sub]
Examples.i [abbreviation, in RecordSub]
Examples.Integer [abbreviation, in Sub]
Examples.j [abbreviation, in RecordSub]
Examples.k [abbreviation, in RecordSub]
Examples.Person [definition, in Sub]
Examples.String [abbreviation, in Sub]
Examples.Student [definition, in Sub]
Examples.subtyping_example_2 [definition, in Sub]
Examples.subtyping_example_1 [definition, in Sub]
Examples.subtyping_example_0 [definition, in Sub]
Examples.subtyping_example_4 [definition, in RecordSub]
Examples.subtyping_example_3 [definition, in RecordSub]
Examples.subtyping_example_2 [definition, in RecordSub]
Examples.subtyping_example_1 [definition, in RecordSub]
Examples.subtyping_example_0 [definition, in RecordSub]
Examples.sub_employee_person [definition, in Sub]
Examples.sub_student_person [definition, in Sub]
Examples.trcd_kj [definition, in RecordSub]
Examples.TRcd_kj [definition, in RecordSub]
Examples.TRcd_j [definition, in RecordSub]
Examples.x [abbreviation, in Sub]
Examples.x [abbreviation, in RecordSub]
Examples.y [abbreviation, in Sub]
Examples.y [abbreviation, in RecordSub]
Examples.z [abbreviation, in Sub]
Examples.z [abbreviation, in RecordSub]
Examples2 [module, in Sub]
Examples2 [module, in RecordSub]
Examples2.typing_example_2 [definition, in RecordSub]
Examples2.typing_example_1 [definition, in RecordSub]
Examples2.typing_example_0 [definition, in RecordSub]
ExAssertions [module, in Hoare]
ExAssertions.as1 [definition, in Hoare]
ExAssertions.as2 [definition, in Hoare]
ExAssertions.as3 [definition, in Hoare]
ExAssertions.as4 [definition, in Hoare]
ExAssertions.as5 [definition, in Hoare]
ExAssertions.as6 [definition, in Hoare]
excluded_middle_irrefutable [lemma, in Logic]
excluded_middle [definition, in Logic]
exists_example_3 [lemma, in MoreLogic]
exists_example_2 [lemma, in MoreLogic]
exists_example_1' [definition, in MoreLogic]
exists_example_1 [definition, in MoreLogic]
exp [definition, in Basics]
expect [definition, in ImpParser]
ExSet [inductive, in MoreInd]
extend [definition, in Sub]
extend [definition, in SfLib]
extend [definition, in RecordSub]
extend_shadow [lemma, in SfLib]
extend_neq [lemma, in SfLib]
extend_eq [lemma, in SfLib]
extract [definition, in Hoare2]
Extraction [library]
ex_intro [constructor, in MoreLogic]
ex_falso_quodlibet [lemma, in Logic]
ex_falso_quodlibet [lemma, in SfLib]
E_Plus [constructor, in Smallstep]
E_Const [constructor, in Smallstep]
E_equiv [constructor, in Equiv]
E_WhileLoop [constructor, in Imp]
E_WhileEnd [constructor, in Imp]
E_IfFalse [constructor, in Imp]
E_IfTrue [constructor, in Imp]
E_Seq [constructor, in Imp]
E_Ass [constructor, in Imp]
E_Skip [constructor, in Imp]
E_Some [constructor, in PE]
E_None [constructor, in PE]

F

factorial [definition, in Basics]
fact_in_coq [definition, in Imp]
false [constructor, in Basics]
False [inductive, in Logic]
false_beq_nat [lemma, in Logic]
False_implies_nonsense [lemma, in Logic]
false_beq_nat [lemma, in SfLib]
False_and_P_imp [lemma, in HoareAsLogic]
filter [definition, in Poly]
filter_even_gt7 [definition, in Poly]
filter_exercise [lemma, in MoreCoq]
firstExpect [definition, in ImpParser]
flat_map [definition, in Poly]
fmostlytrue [definition, in Poly]
fold [definition, in Poly]
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]
fold_map [definition, in Poly]
fold_length_correct [lemma, in Poly]
fold_length [definition, in Poly]
fold_example3 [definition, in Poly]
fold_example2 [definition, in Poly]
fold_example1 [definition, in Poly]
foo' [inductive, in MoreInd]
forallb [definition, in MoreLogic]
free_in_context [lemma, in Norm]
free_in_context [lemma, in Sub]
free_in_context [lemma, in RecordSub]
friday [constructor, in Basics]
fst [definition, in Poly]
ftrue [definition, in Poly]
functional_extensionality [axiom, in Equiv]
f_equal [lemma, in MoreCoq]

G

GenExample [module, in UseTactics]
GenExample.substitution_preserves_typing [lemma, in UseTactics]
gorgeous [inductive, in Prop]
gorgeous_plus13_po [definition, in ProofObjects]
gorgeous__beautiful' [lemma, in MoreInd]
gorgeous_sum [lemma, in Prop]
gorgeous__beautiful_FAILED [lemma, in Prop]
gorgeous__beautiful [lemma, in Prop]
gorgeous_plus13 [lemma, in Prop]
Goto [constructor, in PE]
green [constructor, in MoreInd]
gt_not_le [axiom, in UseAuto]
g_times2 [lemma, in Prop]
g_plus5 [constructor, in Prop]
g_plus3 [constructor, in Prop]
g_0 [constructor, in Prop]

H

halts [definition, in Norm]
has_type [inductive, in Norm]
has_type [inductive, in Sub]
has_type__wf [lemma, in RecordSub]
has_type [inductive, in RecordSub]
has_type_not [definition, in Types]
has_type_1 [definition, in Types]
has_type [inductive, in Types]
hd_opt [definition, in Poly]
helper_g_times2 [lemma, in Prop]
Himp [module, in Equiv]
Himp [module, in Hoare]
Himp.CAsgn [constructor, in Hoare]
Himp.CAss [constructor, in Equiv]
Himp.cequiv [definition, in Equiv]
Himp.ceval [inductive, in Equiv]
Himp.ceval [inductive, in Hoare]
Himp.CHavoc [constructor, in Equiv]
Himp.CHavoc [constructor, in Hoare]
Himp.CIf [constructor, in Equiv]
Himp.CIf [constructor, in Hoare]
Himp.com [inductive, in Equiv]
Himp.com [inductive, in Hoare]
Himp.CSeq [constructor, in Equiv]
Himp.CSeq [constructor, in Hoare]
Himp.CSkip [constructor, in Equiv]
Himp.CSkip [constructor, in Hoare]
Himp.CWhile [constructor, in Equiv]
Himp.CWhile [constructor, in Hoare]
Himp.E_WhileLoop [constructor, in Equiv]
Himp.E_WhileEnd [constructor, in Equiv]
Himp.E_IfFalse [constructor, in Equiv]
Himp.E_IfTrue [constructor, in Equiv]
Himp.E_Seq [constructor, in Equiv]
Himp.E_Ass [constructor, in Equiv]
Himp.E_Skip [constructor, in Equiv]
Himp.E_Havoc [constructor, in Hoare]
Himp.E_WhileLoop [constructor, in Hoare]
Himp.E_WhileEnd [constructor, in Hoare]
Himp.E_IfFalse [constructor, in Hoare]
Himp.E_IfTrue [constructor, in Hoare]
Himp.E_Seq [constructor, in Hoare]
Himp.E_Ass [constructor, in Hoare]
Himp.E_Skip [constructor, in Hoare]
Himp.havoc_example2 [definition, in Equiv]
Himp.havoc_example1 [definition, in Equiv]
Himp.havoc_pre [definition, in Hoare]
Himp.hoare_havoc [lemma, in Hoare]
Himp.hoare_triple [definition, in Hoare]
Himp.pcopy [definition, in Equiv]
Himp.ptwice [definition, in Equiv]
Himp.ptwice_cequiv_pcopy [lemma, in Equiv]
Himp.pXY [definition, in Equiv]
Himp.pXY_cequiv_pYX [lemma, in Equiv]
Himp.pYX [definition, in Equiv]
Himp.p1 [definition, in Equiv]
Himp.p1_p2_equiv [lemma, in Equiv]
Himp.p1_may_diverge [lemma, in Equiv]
Himp.p2 [definition, in Equiv]
Himp.p2_may_diverge [lemma, in Equiv]
Himp.p3 [definition, in Equiv]
Himp.p3_p4_inequiv [lemma, in Equiv]
Himp.p4 [definition, in Equiv]
Himp.p5 [definition, in Equiv]
Himp.p5_p6_equiv [lemma, in Equiv]
Himp.p6 [definition, in Equiv]
{{ _ }} _ {{ _ }} (hoare_spec_scope) [notation, in Hoare]
_ / _ || _ [notation, in Equiv]
_ ;; _ [notation, in Equiv]
_ ::= _ [notation, in Equiv]
_ / _ || _ [notation, in Hoare]
_ ;; _ [notation, in Hoare]
_ ::= _ [notation, in Hoare]
HAVOC _ [notation, in Equiv]
HAVOC _ [notation, in Hoare]
IFB _ THEN _ ELSE _ FI [notation, in Equiv]
IFB _ THEN _ ELSE _ FI [notation, in Hoare]
SKIP [notation, in Equiv]
SKIP [notation, in Hoare]
WHILE _ DO _ END [notation, in Equiv]
WHILE _ DO _ END [notation, in Hoare]
Himp2 [module, in Hoare2]
Himp2.hoare_havoc_weakest [lemma, in Hoare2]
HintsTransitivity [section, in UseAuto]
Hoare [library]
HoareAsLogic [library]
hoare_while [lemma, in Hoare]
hoare_if [lemma, in Hoare]
hoare_asgn_example4 [definition, in Hoare]
hoare_asgn_example3 [definition, in Hoare]
hoare_seq [lemma, in Hoare]
hoare_skip [lemma, in Hoare]
hoare_asgn_example1' [definition, in Hoare]
hoare_consequence [lemma, in Hoare]
hoare_asgn_example1 [definition, in Hoare]
hoare_consequence_post [lemma, in Hoare]
hoare_consequence_pre [lemma, in Hoare]
hoare_asgn_fwd_exists [lemma, in Hoare]
hoare_asgn_fwd [lemma, in Hoare]
hoare_asgn [lemma, in Hoare]
hoare_pre_false [lemma, in Hoare]
hoare_post_true [lemma, in Hoare]
hoare_triple [definition, in Hoare]
hoare_proof_complete [lemma, in HoareAsLogic]
hoare_proof_sound [lemma, in HoareAsLogic]
hoare_proof [inductive, in HoareAsLogic]
hoare_asgn_weakest [lemma, in Hoare2]
Hoare2 [library]
H_Pre_False_deriv [lemma, in HoareAsLogic]
H_Post_True_deriv [lemma, in HoareAsLogic]
H_Consequence_post [lemma, in HoareAsLogic]
H_Consequence_pre [lemma, in HoareAsLogic]
H_Consequence [constructor, in HoareAsLogic]
H_While [constructor, in HoareAsLogic]
H_If [constructor, in HoareAsLogic]
H_Seq [constructor, in HoareAsLogic]
H_Asgn [constructor, in HoareAsLogic]
H_Skip [constructor, in HoareAsLogic]

I

Id [module, in Imp]
Id [constructor, in SfLib]
id [inductive, in SfLib]
identity_assignment' [definition, in Equiv]
identity_assignment [lemma, in Equiv]
identity_assignment_first_try [lemma, in Equiv]
identity_fn_applied_twice [lemma, in Basics]
Id.eq_id [lemma, in Imp]
Id.eq_id_dec [lemma, in Imp]
Id.Id [constructor, in Imp]
Id.id [inductive, in Imp]
Id.neq_id [lemma, in Imp]
If [constructor, in PE]
IFB_false [lemma, in Equiv]
IFB_true [lemma, in Equiv]
IFB_true_simple [lemma, in Equiv]
iff [definition, in Logic]
iff_trans [lemma, in Equiv]
iff_trans [lemma, in Logic]
iff_refl [lemma, in Logic]
iff_sym [lemma, in Logic]
iff_implies [lemma, in Logic]
iff_intro_swap [lemma, in LibTactics]
if_minus_plus [lemma, in Hoare]
if_example [definition, in Hoare]
If1 [module, in Hoare]
If1.CAss [constructor, in Hoare]
If1.ceval [inductive, in Hoare]
If1.CIf [constructor, in Hoare]
If1.CIf1 [constructor, in Hoare]
If1.com [inductive, in Hoare]
If1.CSeq [constructor, in Hoare]
If1.CSkip [constructor, in Hoare]
If1.CWhile [constructor, in Hoare]
If1.E_WhileLoop [constructor, in Hoare]
If1.E_WhileEnd [constructor, in Hoare]
If1.E_IfFalse [constructor, in Hoare]
If1.E_IfTrue [constructor, in Hoare]
If1.E_Seq [constructor, in Hoare]
If1.E_Ass [constructor, in Hoare]
If1.E_Skip [constructor, in Hoare]
If1.hoare_if1_good [lemma, in Hoare]
If1.hoare_triple [definition, in Hoare]
{{ _ }} _ {{ _ }} (hoare_spec_scope) [notation, in Hoare]
_ / _ || _ [notation, in Hoare]
_ ::= _ [notation, in Hoare]
_ ;; _ [notation, in Hoare]
IFB _ THEN _ ELSE _ FI [notation, in Hoare]
IF1 _ THEN _ FI [notation, in Hoare]
SKIP [notation, in Hoare]
WHILE _ DO _ END [notation, in Hoare]
Imp [library]
ImpCEvalFun [library]
implies_to_or [definition, in Logic]
ImpParser [library]
index [definition, in Poly]
index_after_last [lemma, in MoreCoq]
Induction [library]
inequiv_exercise [lemma, in Equiv]
inj_pair2 [axiom, in LibTactics]
instantiation [inductive, in Norm]
instantiation_drop [lemma, in Norm]
instantiation_R [lemma, in Norm]
instantiation_env_closed [lemma, in Norm]
instantiation_domains_match [lemma, in Norm]
IntrovExamples [module, in UseTactics]
IntrovExamples.ceval_deterministic' [lemma, in UseTactics]
IntrovExamples.ceval_deterministic [lemma, in UseTactics]
IntrovExamples.dist_exists_or [lemma, in UseTactics]
IntrovExamples.exists_impl [lemma, in UseTactics]
InvertsExamples [module, in UseTactics]
InvertsExamples.ceval_deterministic' [lemma, in UseTactics]
InvertsExamples.ceval_deterministic [lemma, in UseTactics]
InvertsExamples.skip_left' [lemma, in UseTactics]
InvertsExamples.skip_left [lemma, in UseTactics]
InvertsExamples.typing_nonexample_1 [definition, in UseTactics]
isAlpha [definition, in ImpParser]
isDigit [definition, in ImpParser]
isLowerAlpha [definition, in ImpParser]
isWhite [definition, in ImpParser]
is_fortytwo [definition, in Auto]
is_wp_example [lemma, in Hoare2]
is_wp [definition, in Hoare2]

K

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

L

le [inductive, in MoreInd]
leaf [constructor, in MoreInd]
left [constructor, in MoreLogic]
LeModule [module, in Prop]
LeModule.le [inductive, in Prop]
LeModule.le_S [constructor, in Prop]
LeModule.le_n [constructor, in Prop]
LeModule.test_le3 [lemma, in Prop]
LeModule.test_le2 [lemma, in Prop]
LeModule.test_le1 [lemma, in Prop]
_ <= _ [notation, in Prop]
length [definition, in Poly]
length_is_1 [definition, in Poly]
length_snoc''' [lemma, in MoreCoq]
length_snoc_bad [lemma, in MoreCoq]
length_snoc' [lemma, in MoreCoq]
length' [definition, in Poly]
length'' [definition, in Poly]
le_order [lemma, in Rel]
le_step [lemma, in Rel]
le_antisymmetric [lemma, in Rel]
le_not_symmetric [lemma, in Rel]
le_Sn_n [lemma, in Rel]
le_S_n [lemma, in Rel]
le_Sn_le [lemma, in Rel]
le_trans [lemma, in Rel]
le_reflexive [lemma, in Rel]
le_not_a_partial_function [lemma, in Rel]
le_S [constructor, in MoreInd]
le_n [constructor, in MoreInd]
le_antisym [lemma, in Auto]
le_gt_false [axiom, in UseAuto]
le_not_gt [axiom, in UseAuto]
le_ble_nat [lemma, in Prop]
le_plus_l [lemma, in Prop]
le_trans [lemma, in Prop]
LibTactics [library]
LibTacticsCompatibility [module, in LibTactics]
list [inductive, in Poly]
Lists [library]
list_of_string [definition, in ImpParser]
list123 [definition, in Poly]
list123' [definition, in Poly]
list123'' [definition, in Poly]
list123''' [definition, in Poly]
Logic [library]
lookup [definition, in Norm]
lookup_field_in_value [lemma, in RecordSub]
loop [definition, in Imp]
loop [constructor, in PE]
Loop [module, in PE]
loop_unrolling [lemma, in Equiv]
loop_never_stops [lemma, in Imp]
Loop.ceval_count_sound [lemma, in PE]
Loop.ceval_count_complete [lemma, in PE]
Loop.ceval_count [inductive, in PE]
Loop.E'Ass [constructor, in PE]
Loop.E'IfFalse [constructor, in PE]
Loop.E'IfTrue [constructor, in PE]
Loop.E'Seq [constructor, in PE]
Loop.E'Skip [constructor, in PE]
Loop.E'WhileEnd [constructor, in PE]
Loop.E'WhileLoop [constructor, in PE]
Loop.pe_com_correct [lemma, in PE]
Loop.pe_com_sound [lemma, in PE]
Loop.pe_com_complete [lemma, in PE]
Loop.pe_ceval_count_le [lemma, in PE]
Loop.pe_ceval_count_intro [constructor, in PE]
Loop.pe_ceval_count [inductive, in PE]
Loop.pe_compare_nil_override [lemma, in PE]
Loop.pe_compare_nil_lookup [lemma, in PE]
Loop.pe_loop_example4 [definition, in PE]
Loop.pe_loop_example3 [definition, in PE]
Loop.pe_loop_example2 [definition, in PE]
Loop.pe_loop_example1 [definition, in PE]
Loop.PE_WhileFixed [constructor, in PE]
Loop.PE_WhileFixedLoop [constructor, in PE]
Loop.PE_WhileFixedEnd [constructor, in PE]
Loop.PE_While [constructor, in PE]
Loop.PE_WhileLoop [constructor, in PE]
Loop.PE_WhileEnd [constructor, in PE]
Loop.PE_If [constructor, in PE]
Loop.PE_IfFalse [constructor, in PE]
Loop.PE_IfTrue [constructor, in PE]
Loop.PE_Seq [constructor, in PE]
Loop.PE_AssDynamic [constructor, in PE]
Loop.PE_AssStatic [constructor, in PE]
Loop.PE_Skip [constructor, in PE]
Loop.pe_com [inductive, in PE]
Loop.square_loop [definition, in PE]
_ / _ / _ / _ || _ # _ [notation, in PE]
_ / _ || _ # _ [notation, in PE]
_ / _ || _ / _ / _ [notation, in PE]
lt [definition, in Prop]
ltac_something_show [lemma, in LibTactics]
ltac_something_hide [lemma, in LibTactics]
ltac_something_eq [lemma, in LibTactics]
ltac_something [definition, in LibTactics]
ltac_to_generalize [definition, in LibTactics]
ltac_tag_subst [definition, in LibTactics]
ltac_nat_from_int [definition, in LibTactics]
ltac_database_provide [lemma, in LibTactics]
ltac_database [definition, in LibTactics]
ltac_mark [constructor, in LibTactics]
ltac_Mark [inductive, in LibTactics]
ltac_wilds [constructor, in LibTactics]
ltac_Wilds [inductive, in LibTactics]
ltac_wild [constructor, in LibTactics]
ltac_Wild [inductive, in LibTactics]
ltac_no_arg [constructor, in LibTactics]
ltac_No_arg [inductive, in LibTactics]
lt_trans'' [lemma, in Rel]
lt_trans' [lemma, in Rel]
lt_trans [lemma, in Rel]
lt_S [lemma, in Prop]

M

many [definition, in ImpParser]
many_helper [definition, in ImpParser]
map [definition, in Poly]
map_rev [lemma, in Poly]
mextend [definition, in Norm]
mextend_drop [lemma, in Norm]
mextend_lookup [lemma, in Norm]
minustwo [definition, in Basics]
minus_diag [lemma, in Induction]
monday [constructor, in Basics]
MoreCoq [library]
MoreInd [library]
MoreLogic [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]
multi [inductive, in SfLib]
multistep [definition, 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]
multi_trans [lemma, in SfLib]
multi_R [lemma, in SfLib]
multi_step [constructor, in SfLib]
multi_refl [constructor, in SfLib]
mult_0_r'' [lemma, in MoreInd]
mult_0_r' [lemma, in MoreInd]
mult_S_1 [lemma, in Basics]
mult_0_plus [lemma, in Basics]
mult_0_l [lemma, in Basics]
mult_assoc [lemma, in Induction]
mult_plus_distr_r [lemma, in Induction]
mult_1_l [lemma, in Induction]
mult_comm [lemma, in Induction]
mult_0_plus' [lemma, in Induction]
mult_0_r [lemma, in Induction]
MumbleBaz [module, in Poly]
MumbleBaz.a [constructor, in Poly]
MumbleBaz.b [constructor, in Poly]
MumbleBaz.baz [inductive, in Poly]
MumbleBaz.c [constructor, in Poly]
MumbleBaz.d [constructor, in Poly]
MumbleBaz.e [constructor, in Poly]
MumbleBaz.grumble [inductive, in Poly]
MumbleBaz.mumble [inductive, in Poly]
MumbleBaz.x [constructor, in Poly]
MumbleBaz.y [constructor, in Poly]
myFact [definition, in UseAuto]
mynil [definition, in Poly]
mynil' [definition, in Poly]

N

O

oddb [definition, in Basics]
omega_demo_4 [lemma, in UseAuto]
omega_demo_3 [lemma, in UseAuto]
omega_demo_2 [lemma, in UseAuto]
omega_demo_1 [lemma, in UseAuto]
one_not_beautiful' [lemma, in MoreInd]
one_not_beautiful [lemma, in MoreInd]
one_not_beautiful_FAILED [lemma, in MoreInd]
option [inductive, in Poly]
optionE [inductive, in ImpParser]
option_map [definition, in Poly]
or [inductive, in Logic]
orb [definition, in Basics]
orb_false_elim [lemma, in Logic]
orb_prop [lemma, in Logic]
order [definition, in Rel]
order_matters_2 [lemma, in UseAuto]
order_matters_1 [lemma, in UseAuto]
or_distributes_over_and [lemma, in Logic]
or_distributes_over_and_2 [lemma, in Logic]
or_distributes_over_and_1 [lemma, in Logic]
or_commut' [lemma, in Logic]
or_commut [lemma, in Logic]
or_intror [constructor, in Logic]
or_introl [constructor, in Logic]
other [constructor, in ImpParser]
override [definition, in Poly]
override_shadow' [lemma, in MoreLogic]
override_same' [lemma, in MoreLogic]
override_neq [lemma, in Poly]
override_eq [lemma, in Poly]
override_example [lemma, in Poly]
override_example4 [definition, in Poly]
override_example3 [definition, in Poly]
override_example2 [definition, in Poly]
override_example1 [definition, in Poly]
override_permute [lemma, in MoreCoq]
override_same [lemma, in MoreCoq]
override_shadow [lemma, in MoreCoq]
override' [definition, in MoreLogic]
O_le_n [lemma, in Prop]

P

R

R [definition, in Norm]
R [module, in Prop]
rcd_types_match [lemma, in RecordSub]
real_fact [definition, in Hoare2]
Records [library]
RecordSub [library]
record_tm [inductive, in RecordSub]
record_ty [inductive, in RecordSub]
red [constructor, in MoreInd]
reduce_to_zero_correct' [lemma, in Hoare2]
reduce_to_zero' [definition, in Hoare2]
References [library]
reflexive [definition, in Rel]
refl_step_closure [inductive, in Rel]
refl_equal' [constructor, in MoreInd]
refl_cequiv [lemma, in Equiv]
refl_bequiv [lemma, in Equiv]
refl_aequiv [lemma, in Equiv]
Rel [library]
relation [definition, in Rel]
relation [definition, in SfLib]
Repeat [module, in Auto]
repeat [definition, in Poly]
RepeatExercise [module, in Hoare]
RepeatExercise.CAsgn [constructor, in Hoare]
RepeatExercise.ceval [inductive, in Hoare]
RepeatExercise.CIf [constructor, in Hoare]
RepeatExercise.com [inductive, in Hoare]
RepeatExercise.CRepeat [constructor, in Hoare]
RepeatExercise.CSeq [constructor, in Hoare]
RepeatExercise.CSkip [constructor, in Hoare]
RepeatExercise.CWhile [constructor, in Hoare]
RepeatExercise.ex1_repeat_works [lemma, in Hoare]
RepeatExercise.ex1_repeat [definition, in Hoare]
RepeatExercise.E_WhileLoop [constructor, in Hoare]
RepeatExercise.E_WhileEnd [constructor, in Hoare]
RepeatExercise.E_IfFalse [constructor, in Hoare]
RepeatExercise.E_IfTrue [constructor, in Hoare]
RepeatExercise.E_Seq [constructor, in Hoare]
RepeatExercise.E_Ass [constructor, in Hoare]
RepeatExercise.E_Skip [constructor, in Hoare]
RepeatExercise.hoare_triple [definition, in Hoare]
_ / _ || _ [notation, in Hoare]
_ ::= _ [notation, in Hoare]
_ ;; _ [notation, in Hoare]
IFB _ THEN _ ELSE _ FI [notation, in Hoare]
REPEAT _ UNTIL _ END [notation, in Hoare]
SKIP [notation, in Hoare]
WHILE _ DO _ END [notation, in Hoare]
{{ _ }} _ {{ _ }} [notation, in Hoare]
repeats [inductive, in MoreLogic]
Repeat.CAsgn [constructor, in Auto]
Repeat.ceval [inductive, in Auto]
Repeat.ceval_deterministic' [lemma, in Auto]
Repeat.ceval_deterministic [lemma, in Auto]
Repeat.CIf [constructor, in Auto]
Repeat.com [inductive, in Auto]
Repeat.CRepeat [constructor, in Auto]
Repeat.CSeq [constructor, in Auto]
Repeat.CSkip [constructor, in Auto]
Repeat.CWhile [constructor, in Auto]
Repeat.E_RepeatLoop [constructor, in Auto]
Repeat.E_RepeatEnd [constructor, in Auto]
Repeat.E_WhileLoop [constructor, in Auto]
Repeat.E_WhileEnd [constructor, in Auto]
Repeat.E_IfFalse [constructor, in Auto]
Repeat.E_IfTrue [constructor, in Auto]
Repeat.E_Seq [constructor, in Auto]
Repeat.E_Ass [constructor, in Auto]
Repeat.E_Skip [constructor, in Auto]
_ / _ || _ [notation, in Auto]
_ ::= _ [notation, in Auto]
_ ; _ [notation, in Auto]
IFB _ THEN _ ELSE _ FI [notation, in Auto]
REPEAT _ UNTIL _ END [notation, in Auto]
SKIP [notation, in Auto]
WHILE _ DO _ END [notation, in Auto]
rev [definition, in Poly]
rev_involutive [lemma, in Poly]
rev_snoc [lemma, in Poly]
rev_exercise1 [lemma, in MoreCoq]
rgb [inductive, in MoreInd]
right [constructor, in MoreLogic]
RingDemo [module, in UseAuto]
RingDemo.ring_demo [lemma, in UseAuto]
rm [definition, in LibTactics]
rsc_trans [lemma, in Rel]
rsc_R [lemma, in Rel]
rsc_step [constructor, in Rel]
rsc_refl [constructor, in Rel]
rtcons [constructor, in RecordSub]
RTcons [constructor, in RecordSub]
rtc_rsc_coincide [lemma, in Rel]
rtnil [constructor, in RecordSub]
RTnil [constructor, in RecordSub]
rt_trans [constructor, in Rel]
rt_refl [constructor, in Rel]
rt_step [constructor, in Rel]
R_typable_empty [lemma, in Norm]
R_halts [lemma, in Norm]
R.c1 [constructor, in Prop]
R.c2 [constructor, in Prop]
R.c3 [constructor, in Prop]
R.c4 [constructor, in Prop]
R.c5 [constructor, in Prop]
R.R [inductive, in Prop]

S

T

tabs [constructor, in Norm]
tabs [constructor, in Sub]
tabs [constructor, in RecordSub]
tapp [constructor, in Norm]
tapp [constructor, in Sub]
tapp [constructor, in RecordSub]
TArrow [constructor, in Norm]
TArrow [constructor, in Sub]
TArrow [constructor, in RecordSub]
tass [definition, in Norm]
TBase [constructor, in Sub]
TBase [constructor, in RecordSub]
TBool [constructor, in Norm]
TBool [constructor, in Sub]
TBool [constructor, in Types]
teen [definition, in Prop]
Temp1 [module, in Smallstep]
Temp1.step [inductive, in Smallstep]
Temp1.ST_Plus2 [constructor, in Smallstep]
Temp1.ST_Plus1 [constructor, in Smallstep]
Temp1.ST_PlusConstConst [constructor, in Smallstep]
Temp1.value [inductive, in Smallstep]
Temp1.value_not_same_as_normal_form [lemma, in Smallstep]
Temp1.v_funny [constructor, in Smallstep]
Temp1.v_const [constructor, in Smallstep]
_ ==> _ [notation, in Smallstep]
Temp2 [module, in Smallstep]
Temp2.step [inductive, in Smallstep]
Temp2.ST_Plus2 [constructor, in Smallstep]
Temp2.ST_Plus1 [constructor, in Smallstep]
Temp2.ST_PlusConstConst [constructor, in Smallstep]
Temp2.ST_Funny [constructor, in Smallstep]
Temp2.value [inductive, in Smallstep]
Temp2.value_not_same_as_normal_form [lemma, in Smallstep]
Temp2.v_const [constructor, in Smallstep]
_ ==> _ [notation, in Smallstep]
Temp3 [module, in Smallstep]
Temp3.step [inductive, in Smallstep]
Temp3.ST_Plus1 [constructor, in Smallstep]
Temp3.ST_PlusConstConst [constructor, in Smallstep]
Temp3.value [inductive, in Smallstep]
Temp3.value_not_same_as_normal_form [lemma, in Smallstep]
Temp3.v_const [constructor, in Smallstep]
_ ==> _ [notation, in Smallstep]
Temp4 [module, in Smallstep]
Temp4.bool_step_prop3 [definition, in Smallstep]
Temp4.bool_step_prop2 [definition, in Smallstep]
Temp4.bool_step_prop1 [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_holds [definition, in Smallstep]
Temp4.Temp5.bool_step_prop4 [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]
_ ==> _ [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]
_ ==> _ [notation, in Smallstep]
test_nostutter_4 [definition, in MoreLogic]
test_nostutter_3 [definition, in MoreLogic]
test_nostutter_2 [definition, in MoreLogic]
test_nostutter_1 [definition, in MoreLogic]
test_multistep_4 [lemma, in Smallstep]
test_multistep_3 [lemma, in Smallstep]
test_multistep_2 [lemma, in Smallstep]
test_multistep_1' [lemma, in Smallstep]
test_multistep_1 [lemma, in Smallstep]
test_blt_nat3 [definition, in Basics]
test_blt_nat2 [definition, in Basics]
test_blt_nat1 [definition, in Basics]
test_ble_nat3 [definition, in Basics]
test_ble_nat2 [definition, in Basics]
test_ble_nat1 [definition, in Basics]
test_factorial2 [definition, in Basics]
test_factorial1 [definition, in Basics]
test_oddb2 [definition, in Basics]
test_oddb1 [definition, in Basics]
test_andb34 [definition, in Basics]
test_andb33 [definition, in Basics]
test_andb32 [definition, in Basics]
test_andb31 [definition, in Basics]
test_nandb4 [definition, in Basics]
test_nandb3 [definition, in Basics]
test_nandb2 [definition, in Basics]
test_nandb1 [definition, in Basics]
test_orb4 [definition, in Basics]
test_orb3 [definition, in Basics]
test_orb2 [definition, in Basics]
test_orb1 [definition, in Basics]
test_next_weekday [definition, in Basics]
test_fold_length1 [definition, in Poly]
test_flat_map1 [definition, in Poly]
test_map3 [definition, in Poly]
test_map2 [definition, in Poly]
test_map1 [definition, in Poly]
test_partition2 [definition, in Poly]
test_partition1 [definition, in Poly]
test_filter_even_gt7_2 [definition, in Poly]
test_filter_even_gt7_1 [definition, in Poly]
test_filter2' [definition, in Poly]
test_anon_fun' [definition, in Poly]
test_countoddmembers'3 [definition, in Poly]
test_countoddmembers'2 [definition, in Poly]
test_countoddmembers'1 [definition, in Poly]
test_filter2 [definition, in Poly]
test_filter1 [definition, in Poly]
test_plus3'' [definition, in Poly]
test_plus3' [definition, in Poly]
test_plus3 [definition, in Poly]
test_doit3times' [definition, in Poly]
test_doit3times [definition, in Poly]
test_hd_opt2 [definition, in Poly]
test_hd_opt1 [definition, in Poly]
test_index3 [definition, in Poly]
test_index2 [definition, in Poly]
test_index1 [definition, in Poly]
test_split [definition, in Poly]
test_repeat1 [definition, in Poly]
test_rev2 [definition, in Poly]
test_rev1 [definition, in Poly]
test_length2 [definition, in Poly]
test_length1 [definition, in Poly]
test_ceval [definition, in ImpCEvalFun]
test_pe_bexp2 [definition, in PE]
test_pe_bexp1 [definition, in PE]
test_pe_override [definition, in PE]
test_pe_aexp1 [definition, in PE]
text_pe_aexp2 [definition, in PE]
tfalse [constructor, in Norm]
tfalse [constructor, in Sub]
tfalse [constructor, in Types]
tfst [constructor, in Norm]
three_is_beautiful [lemma, in Prop]
thursday [constructor, in Basics]
tif [constructor, in Norm]
tif [constructor, in Sub]
tif [constructor, in Types]
tiszero [constructor, in Types]
tlookup [definition, in RecordSub]
Tlookup [definition, in RecordSub]
tm [inductive, in Smallstep]
tm [inductive, in Norm]
tm [inductive, in Sub]
tm [inductive, in RecordSub]
tm [inductive, in Types]
TNat [constructor, in Types]
token [definition, in ImpParser]
tokenize [definition, in ImpParser]
tokenize_ex1 [definition, in ImpParser]
tokenize_helper [definition, in ImpParser]
tot [constructor, in SfLib]
total_relation [inductive, in SfLib]
tpair [constructor, in Norm]
tpred [constructor, in Types]
TProd [constructor, in Norm]
tproj [constructor, in RecordSub]
transitive [definition, in Rel]
transitivity_workaround_2 [lemma, in UseAuto]
transitivity_workaround_1 [lemma, in UseAuto]
transitivity_bad_hint_1 [lemma, in UseAuto]
trans_eq_example' [definition, in ProofObjects]
trans_cequiv [lemma, in Equiv]
trans_bequiv [lemma, in Equiv]
trans_aequiv [lemma, in Equiv]
trans_eq_exercise [definition, in MoreCoq]
trans_eq_example' [definition, in MoreCoq]
trans_eq [lemma, in MoreCoq]
trans_eq_example [definition, in MoreCoq]
trcons [constructor, in RecordSub]
TRCons [constructor, in RecordSub]
tree [inductive, in MoreInd]
trnil [constructor, in RecordSub]
TRNil [constructor, in RecordSub]
true [constructor, in Basics]
true_for_all_numbers [definition, in Prop]
true_for_zero [definition, in Prop]
tsnd [constructor, in Norm]
tsucc [constructor, in Types]
TTop [constructor, in Sub]
TTop [constructor, in RecordSub]
ttrue [constructor, in Norm]
ttrue [constructor, in Sub]
ttrue [constructor, in Types]
tuesday [constructor, in Basics]
tunit [constructor, in Sub]
TUnit [constructor, in Sub]
tvar [constructor, in Norm]
tvar [constructor, in Sub]
tvar [constructor, in RecordSub]
ty [inductive, in Norm]
ty [inductive, in Sub]
ty [inductive, in RecordSub]
ty [inductive, in Types]
typ [axiom, in UseAuto]
typable_empty__closed [lemma, in Norm]
Typechecking [library]
Types [library]
typing_inversion_unit [lemma, in Sub]
typing_inversion_if [lemma, in Sub]
typing_inversion_false [lemma, in Sub]
typing_inversion_true [lemma, in Sub]
typing_inversion_app [lemma, in Sub]
typing_inversion_var [lemma, in Sub]
typing_inversion_abs [lemma, in Sub]
typing_inversion_rcons [lemma, in RecordSub]
typing_inversion_proj [lemma, in RecordSub]
typing_inversion_abs [lemma, in RecordSub]
typing_inversion_app [lemma, in RecordSub]
typing_inversion_var [lemma, in RecordSub]
tzero [constructor, in Types]
T_If [constructor, in Norm]
T_False [constructor, in Norm]
T_True [constructor, in Norm]
T_Snd [constructor, in Norm]
T_Fst [constructor, in Norm]
T_Pair [constructor, in Norm]
T_App [constructor, in Norm]
T_Abs [constructor, in Norm]
T_Var [constructor, in Norm]
T_Sub [constructor, in Sub]
T_Unit [constructor, in Sub]
T_If [constructor, in Sub]
T_False [constructor, in Sub]
T_True [constructor, in Sub]
T_App [constructor, in Sub]
T_Abs [constructor, in Sub]
T_Var [constructor, in Sub]
T_RCons [constructor, in RecordSub]
T_RNil [constructor, in RecordSub]
T_Sub [constructor, in RecordSub]
T_Proj [constructor, in RecordSub]
T_App [constructor, in RecordSub]
T_Abs [constructor, in RecordSub]
T_Var [constructor, in RecordSub]
T_Iszero [constructor, in Types]
T_Pred [constructor, in Types]
T_Succ [constructor, in Types]
T_Zero [constructor, in Types]
T_If [constructor, in Types]
T_False [constructor, in Types]
T_True [constructor, in Types]

U

uncurry_curry [lemma, in Poly]
UnfoldsExample [module, in UseTactics]
UnfoldsExample.bexp_eval_true [lemma, in UseTactics]
unfold_example [lemma, in Poly]
unfold_example_bad [lemma, in Poly]
update [definition, in Imp]
update_permute [lemma, in Imp]
update_same [lemma, in Imp]
update_shadow [lemma, in Imp]
update_example [lemma, in Imp]
update_neq [lemma, in Imp]
update_eq [lemma, in Imp]
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_not_used_in_aexp [inductive, in Equiv]
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_false [constructor, in Norm]
v_true [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

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_true [lemma, in Equiv]
WHILE_true_nonterm [lemma, in Equiv]
WHILE_false [lemma, in Equiv]
while_example [definition, in Hoare]
white [constructor, in ImpParser]
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]
yes [constructor, in MoreInd]
yesno [inductive, in MoreInd]

Z

Z [definition, in Imp]
zero_nbeq_plus_1 [lemma, in Basics]
zero_nbeq_S [lemma, in Induction]

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]
IFB _ THEN _ ELSE _ FI [in Imp]
SKIP [in Imp]
WHILE _ DO _ END [in Imp]

C

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

H

{{ _ }} _ {{ _ }} (hoare_spec_scope) [in Hoare]
_ / _ || _ [in Equiv]
_ ;; _ [in Equiv]
_ ::= _ [in Equiv]
_ / _ || _ [in Hoare]
_ ;; _ [in Hoare]
_ ::= _ [in Hoare]
HAVOC _ [in Equiv]
HAVOC _ [in Hoare]
IFB _ THEN _ ELSE _ FI [in Equiv]
IFB _ THEN _ ELSE _ FI [in Hoare]
SKIP [in Equiv]
SKIP [in Hoare]
WHILE _ DO _ END [in Equiv]
WHILE _ DO _ END [in Hoare]

I

{{ _ }} _ {{ _ }} (hoare_spec_scope) [in Hoare]
_ / _ || _ [in Hoare]
_ ::= _ [in Hoare]
_ ;; _ [in Hoare]
IFB _ THEN _ ELSE _ FI [in Hoare]
IF1 _ THEN _ FI [in Hoare]
SKIP [in Hoare]
WHILE _ DO _ END [in Hoare]

L

_ <= _ [in Prop]
_ / _ / _ / _ || _ # _ [in PE]
_ / _ || _ # _ [in PE]
_ / _ || _ / _ / _ [in PE]

N

_ ++ _ [in Lists]
_ :: _ [in Lists]
( _ , _ ) [in Lists]
[ _ ; .. ; _ ] [in Lists]
[ ] [in Lists]

R

_ / _ || _ [in Hoare]
_ ::= _ [in Hoare]
_ ;; _ [in Hoare]
IFB _ THEN _ ELSE _ FI [in Hoare]
REPEAT _ UNTIL _ END [in Hoare]
SKIP [in Hoare]
WHILE _ DO _ END [in Hoare]
{{ _ }} _ {{ _ }} [in Hoare]
_ / _ || _ [in Auto]
_ ::= _ [in Auto]
_ ; _ [in Auto]
IFB _ THEN _ ELSE _ FI [in Auto]
REPEAT _ UNTIL _ END [in Auto]
SKIP [in Auto]
WHILE _ DO _ END [in Auto]

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 [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]

G

GenExample [in UseTactics]

H

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

I

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

L

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

M

MumbleBaz [in Poly]

N

NaryExamples [in UseTactics]
NatList [in Lists]
NatList.Dictionary [in Lists]

P

Playground1 [in Basics]
Playground2 [in Basics]
PreservationProgressReferences [in UseAuto]
PreservationProgressStlc [in UseAuto]

R

R [in Prop]
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

E

Equiv
Extraction

H

Hoare
HoareAsLogic
Hoare2

I

Imp
ImpCEvalFun
ImpParser
Induction

L

LibTactics
Lists
Logic

M

MoreCoq
MoreInd
MoreLogic
MoreStlc

N

Norm

P

PE
Poly
Postscript
Preface
ProofObjects
Prop

R

Records
RecordSub
References
Rel

S

SfLib
Smallstep
Stlc
StlcProp
Sub
Symbols

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.ev100 [in Imp]
AExp.ev100' [in Imp]
AExp.foo [in Imp]
AExp.foo' [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.optimize_0plus_sound [in Imp]
AExp.silly1 [in Imp]
AExp.silly2 [in Imp]
all3_spec [in Induction]
always_loop_hoare [in Hoare]
andb_eq_orb [in Basics]
andb_false [in Logic]
andb_true_intro [in Logic]
andb_prop [in Logic]
andb_false_r [in Induction]
andb_true_elim2 [in Induction]
andb_true_elim1 [in Induction]
andb_true [in SfLib]
andb_true_elim2 [in SfLib]
andb_true_elim1 [in SfLib]
and_commut [in ProofObjects]
and_example [in ProofObjects]
and_assoc [in Logic]
and_commut [in Logic]
and_example' [in Logic]
and_example [in Logic]
appears_in_app_split [in MoreLogic]
appears_in_app [in MoreLogic]
app_length [in MoreLogic]
app_appears_in [in MoreLogic]
app_length_twice [in MoreCoq]
app_length_cons [in MoreCoq]
assign_aequiv [in Equiv]
assign_removes [in PE]

B

bassn_eval_false [in HoareAsLogic]
beautiful__gorgeous [in Prop]
beautiful_plus_eight [in Prop]
bequiv_example [in Equiv]
beq_nat_false [in Logic]
beq_nat_refl [in Induction]
beq_nat_trans [in MoreCoq]
beq_nat_sym [in MoreCoq]
beq_nat_true [in MoreCoq]
beq_nat_0_r [in MoreCoq]
beq_nat_0_l [in MoreCoq]
beq_nat_sym [in SfLib]
bexp_eval_false [in Hoare]
bexp_eval_true [in Hoare]
ble_nat_refl [in Induction]
ble_nat_false [in SfLib]
ble_nat_true [in SfLib]
ble_nat_false_iff [in Hoare2]
ble_nat_true_iff [in Hoare2]
ble_nat_false [in Prop]
ble_nat_true_trans [in Prop]
ble_nat_true [in Prop]
bool_fn_applied_thrice [in MoreCoq]
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]
b_plus3 [in ProofObjects]
b_timesm [in Prop]
b_times2 [in Prop]

C

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]
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 MoreLogic]
dist_not_exists [in MoreLogic]
double_neg [in Logic]
double_plus [in Induction]
double_induction [in MoreCoq]
double_injective_take2 [in MoreCoq]
double_injective_take2_FAILED [in MoreCoq]
double_injective [in MoreCoq]
double_injective_FAILED [in MoreCoq]
double_even [in Prop]
duplicate_subst [in Norm]
dup_lemma [in LibTactics]

E

eight_is_beautiful'' [in ProofObjects]
eight_is_beautiful' [in ProofObjects]
eight_is_beautiful [in ProofObjects]
eight_is_beautiful [in Prop]
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]
eq_nat_dec [in MoreLogic]
eq_add_S [in MoreCoq]
eq_id [in SfLib]
eq_id_dec [in SfLib]
evalF_eval [in Smallstep]
eval__multistep [in Smallstep]
eval_assign [in PE]
evenb_n__oddb_Sn [in Induction]
even__ev' [in MoreInd]
even5_nonsense [in Prop]
ev_not_ev_S [in SfLib]
ev_plus_plus [in Prop]
ev_ev__ev [in Prop]
ev_minus2 [in Prop]
ev_sum [in Prop]
ev__even [in Prop]
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]
excluded_middle_irrefutable [in Logic]
exists_example_3 [in MoreLogic]
exists_example_2 [in MoreLogic]
extend_shadow [in SfLib]
extend_neq [in SfLib]
extend_eq [in SfLib]
ex_falso_quodlibet [in Logic]
ex_falso_quodlibet [in SfLib]

F

false_beq_nat [in Logic]
False_implies_nonsense [in Logic]
false_beq_nat [in SfLib]
False_and_P_imp [in HoareAsLogic]
filter_exercise [in MoreCoq]
fold_constants_com_sound [in Equiv]
fold_constants_bexp_sound [in Equiv]
fold_constants_aexp_sound [in Equiv]
fold_length_correct [in Poly]
free_in_context [in Norm]
free_in_context [in Sub]
free_in_context [in RecordSub]
f_equal [in MoreCoq]

G

GenExample.substitution_preserves_typing [in UseTactics]
gorgeous__beautiful' [in MoreInd]
gorgeous_sum [in Prop]
gorgeous__beautiful_FAILED [in Prop]
gorgeous__beautiful [in Prop]
gorgeous_plus13 [in Prop]
g_times2 [in Prop]

H

has_type__wf [in RecordSub]
helper_g_times2 [in Prop]
Himp.hoare_havoc [in Hoare]
Himp.ptwice_cequiv_pcopy [in Equiv]
Himp.pXY_cequiv_pYX [in Equiv]
Himp.p1_p2_equiv [in Equiv]
Himp.p1_may_diverge [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_while [in Hoare]
hoare_if [in Hoare]
hoare_seq [in Hoare]
hoare_skip [in Hoare]
hoare_consequence [in Hoare]
hoare_consequence_post [in Hoare]
hoare_consequence_pre [in Hoare]
hoare_asgn_fwd_exists [in Hoare]
hoare_asgn_fwd [in Hoare]
hoare_asgn [in Hoare]
hoare_pre_false [in Hoare]
hoare_post_true [in Hoare]
hoare_proof_complete [in HoareAsLogic]
hoare_proof_sound [in HoareAsLogic]
hoare_asgn_weakest [in Hoare2]
H_Pre_False_deriv [in HoareAsLogic]
H_Post_True_deriv [in HoareAsLogic]
H_Consequence_post [in HoareAsLogic]
H_Consequence_pre [in HoareAsLogic]

I

identity_assignment [in Equiv]
identity_assignment_first_try [in Equiv]
identity_fn_applied_twice [in Basics]
Id.eq_id [in Imp]
Id.eq_id_dec [in Imp]
Id.neq_id [in Imp]
IFB_false [in Equiv]
IFB_true [in Equiv]
IFB_true_simple [in Equiv]
iff_trans [in Equiv]
iff_trans [in Logic]
iff_refl [in Logic]
iff_sym [in Logic]
iff_implies [in Logic]
iff_intro_swap [in LibTactics]
if_minus_plus [in Hoare]
If1.hoare_if1_good [in Hoare]
index_after_last [in MoreCoq]
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

LeModule.test_le3 [in Prop]
LeModule.test_le2 [in Prop]
LeModule.test_le1 [in Prop]
length_snoc''' [in MoreCoq]
length_snoc_bad [in MoreCoq]
length_snoc' [in MoreCoq]
le_order [in Rel]
le_step [in Rel]
le_antisymmetric [in Rel]
le_not_symmetric [in Rel]
le_Sn_n [in Rel]
le_S_n [in Rel]
le_Sn_le [in Rel]
le_trans [in Rel]
le_reflexive [in Rel]
le_not_a_partial_function [in Rel]
le_antisym [in Auto]
le_ble_nat [in Prop]
le_plus_l [in Prop]
le_trans [in Prop]
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_override [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]
lt_trans'' [in Rel]
lt_trans' [in Rel]
lt_trans [in Rel]
lt_S [in Prop]

M

map_rev [in Poly]
mextend_drop [in Norm]
mextend_lookup [in Norm]
minus_diag [in Induction]
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]
multi_trans [in SfLib]
multi_R [in SfLib]
mult_0_r'' [in MoreInd]
mult_0_r' [in MoreInd]
mult_S_1 [in Basics]
mult_0_plus [in Basics]
mult_0_l [in Basics]
mult_assoc [in Induction]
mult_plus_distr_r [in Induction]
mult_1_l [in Induction]
mult_comm [in Induction]
mult_0_plus' [in Induction]
mult_0_r [in Induction]

N

O

omega_demo_4 [in UseAuto]
omega_demo_3 [in UseAuto]
omega_demo_2 [in UseAuto]
omega_demo_1 [in UseAuto]
one_not_beautiful' [in MoreInd]
one_not_beautiful [in MoreInd]
one_not_beautiful_FAILED [in MoreInd]
orb_false_elim [in Logic]
orb_prop [in Logic]
order_matters_2 [in UseAuto]
order_matters_1 [in UseAuto]
or_distributes_over_and [in Logic]
or_distributes_over_and_2 [in Logic]
or_distributes_over_and_1 [in Logic]
or_commut' [in Logic]
or_commut [in Logic]
override_shadow' [in MoreLogic]
override_same' [in MoreLogic]
override_neq [in Poly]
override_eq [in Poly]
override_example [in Poly]
override_permute [in MoreCoq]
override_same [in MoreCoq]
override_shadow [in MoreCoq]
O_le_n [in Prop]

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]
Repeat.ceval_deterministic' [in Auto]
Repeat.ceval_deterministic [in Auto]
rev_involutive [in Poly]
rev_snoc [in Poly]
rev_exercise1 [in MoreCoq]
RingDemo.ring_demo [in UseAuto]
rsc_trans [in Rel]
rsc_R [in Rel]
rtc_rsc_coincide [in Rel]
R_typable_empty [in Norm]
R_halts [in Norm]

S

T

U

uncurry_curry [in Poly]
UnfoldsExample.bexp_eval_true [in UseTactics]
unfold_example [in Poly]
unfold_example_bad [in Poly]
update_permute [in Imp]
update_same [in Imp]
update_shadow [in Imp]
update_example [in Imp]
update_neq [in Imp]
update_eq [in Imp]

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 [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

zero_nbeq_plus_1 [in Basics]
zero_nbeq_S [in Induction]

Constructor Index

A

B

BAnd [in Imp]
bempty [in MoreInd]
BEq [in Imp]
BFalse [in Imp]
BLe [in Imp]
bleaf [in MoreInd]
blue [in MoreInd]
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_AndStep [in Smallstep]
BS_AndTrueStep [in Smallstep]
BS_AndFalse [in Smallstep]
BS_AndTrueFalse [in Smallstep]
BS_AndTrueTrue [in Smallstep]
BS_NotStep [in Smallstep]
BS_NotFalse [in Smallstep]
BS_NotTrue [in Smallstep]
BS_LtEq2 [in Smallstep]
BS_LtEq1 [in Smallstep]
BS_LtEq [in Smallstep]
BS_Eq2 [in Smallstep]
BS_Eq1 [in Smallstep]
BS_Eq [in Smallstep]
BTrue [in Imp]
bv_false [in Types]
bv_true [in Types]
b_sum [in Prop]
b_5 [in Prop]
b_3 [in Prop]
b_0 [in Prop]

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

entry [in PE]
ev_SS [in SfLib]
ev_0 [in SfLib]
ev_SS [in Prop]
ev_0 [in Prop]
ex_intro [in MoreLogic]
E_Plus [in Smallstep]
E_Const [in Smallstep]
E_equiv [in Equiv]
E_WhileLoop [in Imp]
E_WhileEnd [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

false [in Basics]
friday [in Basics]

G

Goto [in PE]
green [in MoreInd]
g_plus5 [in Prop]
g_plus3 [in Prop]
g_0 [in Prop]

H

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

I

Id [in SfLib]
Id.Id [in Imp]
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_WhileLoop [in Hoare]
If1.E_WhileEnd [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]

L

leaf [in MoreInd]
left [in MoreLogic]
LeModule.le_S [in Prop]
LeModule.le_n [in Prop]
le_S [in MoreInd]
le_n [in MoreInd]
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_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_WhileLoop [in PE]
Loop.PE_WhileEnd [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_mark [in LibTactics]
ltac_wilds [in LibTactics]
ltac_wild [in LibTactics]
ltac_no_arg [in LibTactics]

M

monday [in Basics]
multi_step [in Smallstep]
multi_refl [in Smallstep]
multi_step [in SfLib]
multi_refl [in SfLib]
MumbleBaz.a [in Poly]
MumbleBaz.b [in Poly]
MumbleBaz.c [in Poly]
MumbleBaz.d [in Poly]
MumbleBaz.e [in Poly]
MumbleBaz.x [in Poly]
MumbleBaz.y [in Poly]

N

NatList.cons [in Lists]
NatList.Dictionary.empty [in Lists]
NatList.Dictionary.record [in Lists]
NatList.nil [in Lists]
NatList.None [in Lists]
NatList.pair [in Lists]
NatList.Some [in Lists]
nbranch [in MoreInd]
ncons [in MoreInd]
ne_2 [in Prop]
ne_1 [in Prop]
nil [in Poly]
nn [in SfLib]
nn [in Prop]
nnil [in MoreInd]
nnil1 [in MoreInd]
no [in MoreInd]
node [in MoreInd]
None [in Poly]
NoneE [in ImpParser]
nsnoc1 [in MoreInd]
nv_succ [in Types]
nv_zero [in Types]

O

or_intror [in Logic]
or_introl [in Logic]
other [in ImpParser]

P

P [in Smallstep]
pair [in Poly]
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]
Playground1.O [in Basics]
Playground1.S [in Basics]

R

S

T

V

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_false [in Norm]
v_true [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

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

Y

yes [in MoreInd]

Axiom Index

E

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

F

functional_extensionality [in Equiv]

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]

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.aevalR [in Imp]
AExp.aexp [in Imp]
AExp.bexp [in Imp]
all [in MoreLogic]
and [in Logic]
appears_in [in MoreLogic]
appears_free_in [in Norm]
appears_free_in [in Sub]
appears_in [in SfLib]
appears_free_in [in RecordSub]
astep [in Smallstep]
aval [in Smallstep]

B

beautiful [in Prop]
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 MoreInd]

C

ceval [in Imp]
ceval' [in Equiv]
chartype [in ImpParser]
CImp.com [in Smallstep]
CImp.cstep [in Smallstep]
clos_refl_trans [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

empty_relation [in SfLib]
eq' [in MoreInd]
ev [in SfLib]
ev [in Prop]
eval [in Smallstep]
ex [in MoreLogic]
ExSet [in MoreInd]

F

False [in Logic]
foo' [in MoreInd]

G

gorgeous [in Prop]

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]
hoare_proof [in HoareAsLogic]

I

id [in SfLib]
Id.id [in Imp]
If1.ceval [in Hoare]
If1.com [in Hoare]
instantiation [in Norm]

L

le [in MoreInd]
LeModule.le [in Prop]
list [in Poly]
Loop.ceval_count [in PE]
Loop.pe_ceval_count [in PE]
Loop.pe_com [in PE]
ltac_Mark [in LibTactics]
ltac_Wilds [in LibTactics]
ltac_Wild [in LibTactics]
ltac_No_arg [in LibTactics]

M

multi [in Smallstep]
multi [in SfLib]
MumbleBaz.baz [in Poly]
MumbleBaz.grumble [in Poly]
MumbleBaz.mumble [in Poly]

N

natlist [in MoreInd]
NatList.Dictionary.dictionary [in Lists]
NatList.natlist [in Lists]
NatList.natoption [in Lists]
NatList.natprod [in Lists]
natlist1 [in MoreInd]
next_nat [in SfLib]
next_even [in Prop]
next_nat [in Prop]
nostutter [in MoreLogic]
no_whilesR [in Imp]
nvalue [in Types]

O

option [in Poly]
optionE [in ImpParser]
or [in Logic]

P

parity_label [in PE]
peval [in PE]
pe_peval [in PE]
pe_ceval [in PE]
pe_com [in PE]
Playground1.nat [in Basics]
prod [in Poly]

R

record_tm [in RecordSub]
record_ty [in RecordSub]
refl_step_closure [in Rel]
RepeatExercise.ceval [in Hoare]
RepeatExercise.com [in Hoare]
repeats [in MoreLogic]
Repeat.ceval [in Auto]
Repeat.com [in Auto]
rgb [in MoreInd]
R.R [in Prop]

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]
total_relation [in SfLib]
tree [in MoreInd]
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]

Y

yesno [in MoreInd]

Section Index

D

DemoAbsurd1 [in UseAuto]

E

equatesLemma [in LibTactics]

H

HintsTransitivity [in UseAuto]

S

STLCRef.RefsAndNontermination [in References]

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

B

bassn [in Hoare]
beatiful_plus3'' [in ProofObjects]
beautiful_iff_gorgeous [in ProofObjects]
beautiful_plus3' [in ProofObjects]
beautiful_plus3 [in ProofObjects]
bequiv [in Equiv]
beq_nat [in Basics]
between [in Prop]
beval [in Imp]
bexp1 [in Imp]
bignumber [in ImpParser]
ble_nat [in Basics]
ble_nat [in SfLib]
blt_nat [in Basics]
btrans_sound [in Equiv]
build_symtable [in ImpParser]
b_times2' [in ProofObjects]
b_plus3'' [in ProofObjects]
b_plus3' [in ProofObjects]

C

cequiv [in Equiv]
cequiv' [in Equiv]
ceval_example2 [in Imp]
ceval_example1 [in Imp]
ceval_fun_no_while [in Imp]
ceval_step [in ImpCEvalFun]
ceval_step3 [in ImpCEvalFun]
ceval_step2 [in ImpCEvalFun]
ceval_step1 [in ImpCEvalFun]
CImp.cmultistep [in Smallstep]
CImp.par_loop_example_2 [in Smallstep]
CImp.par_loop_example_0 [in Smallstep]
CImp.par_loop [in Smallstep]
classic [in Logic]
classifyChar [in ImpParser]
closed [in Norm]
closed_env [in Norm]
combine [in Poly]
combine_odd_even [in Prop]
compiler_is_correct_statement [in Smallstep]
congruence_example [in Equiv]
conj_fact [in ProofObjects]
constfun [in Poly]
constfun_example2 [in Poly]
constfun_example1 [in Poly]
context [in Norm]
context [in Sub]
context [in RecordSub]
countoddmembers' [in Poly]
ctrans_sound [in Equiv]

D

dec_correct [in Hoare2]
dec_while [in Hoare2]
deterministic [in SfLib]
de_morgan_not_and_not [in Logic]
doit3times [in Poly]
double [in Induction]
drop [in Norm]

E

F

factorial [in Basics]
fact_in_coq [in Imp]
filter [in Poly]
filter_even_gt7 [in Poly]
firstExpect [in ImpParser]
flat_map [in Poly]
fmostlytrue [in Poly]
fold [in Poly]
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]
fold_map [in Poly]
fold_length [in Poly]
fold_example3 [in Poly]
fold_example2 [in Poly]
fold_example1 [in Poly]
forallb [in MoreLogic]
fst [in Poly]
ftrue [in Poly]

G

gorgeous_plus13_po [in ProofObjects]

H

halts [in Norm]
has_type_not [in Types]
has_type_1 [in Types]
hd_opt [in Poly]
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.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_example4 [in Hoare]
hoare_asgn_example3 [in Hoare]
hoare_asgn_example1' [in Hoare]
hoare_asgn_example1 [in Hoare]
hoare_triple [in Hoare]

I

identity_assignment' [in Equiv]
iff [in Logic]
if_example [in Hoare]
If1.hoare_triple [in Hoare]
implies_to_or [in Logic]
index [in Poly]
InvertsExamples.typing_nonexample_1 [in UseTactics]
isAlpha [in ImpParser]
isDigit [in ImpParser]
isLowerAlpha [in ImpParser]
isWhite [in ImpParser]
is_fortytwo [in Auto]
is_wp [in Hoare2]

K

keval [in PE]
keval_example [in PE]

L

length [in Poly]
length_is_1 [in Poly]
length' [in Poly]
length'' [in Poly]
list_of_string [in ImpParser]
list123 [in Poly]
list123' [in Poly]
list123'' [in Poly]
list123''' [in Poly]
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]
lt [in Prop]
ltac_something [in LibTactics]
ltac_to_generalize [in LibTactics]
ltac_tag_subst [in LibTactics]
ltac_nat_from_int [in LibTactics]
ltac_database [in LibTactics]

M

many [in ImpParser]
many_helper [in ImpParser]
map [in Poly]
mextend [in Norm]
minustwo [in Basics]
msubst [in Norm]
multistep [in Smallstep]
multistep [in Types]
myFact [in UseAuto]
mynil [in Poly]
mynil' [in Poly]

N

O

oddb [in Basics]
option_map [in Poly]
orb [in Basics]
order [in Rel]
override [in Poly]
override_example4 [in Poly]
override_example3 [in Poly]
override_example2 [in Poly]
override_example1 [in Poly]
override' [in MoreLogic]

P

R

R [in Norm]
real_fact [in Hoare2]
reduce_to_zero' [in Hoare2]
reflexive [in Rel]
relation [in Rel]
relation [in SfLib]
repeat [in Poly]
RepeatExercise.ex1_repeat [in Hoare]
RepeatExercise.hoare_triple [in Hoare]
rev [in Poly]
rm [in LibTactics]

S

T

tass [in Norm]
teen [in Prop]
Temp4.bool_step_prop3 [in Smallstep]
Temp4.bool_step_prop2 [in Smallstep]
Temp4.bool_step_prop1 [in Smallstep]
Temp4.Temp5.bool_step_prop4_holds [in Smallstep]
Temp4.Temp5.bool_step_prop4 [in Smallstep]
test_nostutter_4 [in MoreLogic]
test_nostutter_3 [in MoreLogic]
test_nostutter_2 [in MoreLogic]
test_nostutter_1 [in MoreLogic]
test_blt_nat3 [in Basics]
test_blt_nat2 [in Basics]
test_blt_nat1 [in Basics]
test_ble_nat3 [in Basics]
test_ble_nat2 [in Basics]
test_ble_nat1 [in Basics]
test_factorial2 [in Basics]
test_factorial1 [in Basics]
test_oddb2 [in Basics]
test_oddb1 [in Basics]
test_andb34 [in Basics]
test_andb33 [in Basics]
test_andb32 [in Basics]
test_andb31 [in Basics]
test_nandb4 [in Basics]
test_nandb3 [in Basics]
test_nandb2 [in Basics]
test_nandb1 [in Basics]
test_orb4 [in Basics]
test_orb3 [in Basics]
test_orb2 [in Basics]
test_orb1 [in Basics]
test_next_weekday [in Basics]
test_fold_length1 [in Poly]
test_flat_map1 [in Poly]
test_map3 [in Poly]
test_map2 [in Poly]
test_map1 [in Poly]
test_partition2 [in Poly]
test_partition1 [in Poly]
test_filter_even_gt7_2 [in Poly]
test_filter_even_gt7_1 [in Poly]
test_filter2' [in Poly]
test_anon_fun' [in Poly]
test_countoddmembers'3 [in Poly]
test_countoddmembers'2 [in Poly]
test_countoddmembers'1 [in Poly]
test_filter2 [in Poly]
test_filter1 [in Poly]
test_plus3'' [in Poly]
test_plus3' [in Poly]
test_plus3 [in Poly]
test_doit3times' [in Poly]
test_doit3times [in Poly]
test_hd_opt2 [in Poly]
test_hd_opt1 [in Poly]
test_index3 [in Poly]
test_index2 [in Poly]
test_index1 [in Poly]
test_split [in Poly]
test_repeat1 [in Poly]
test_rev2 [in Poly]
test_rev1 [in Poly]
test_length2 [in Poly]
test_length1 [in Poly]
test_ceval [in ImpCEvalFun]
test_pe_bexp2 [in PE]
test_pe_bexp1 [in PE]
test_pe_override [in PE]
test_pe_aexp1 [in PE]
text_pe_aexp2 [in PE]
tlookup [in RecordSub]
Tlookup [in RecordSub]
token [in ImpParser]
tokenize [in ImpParser]
tokenize_ex1 [in ImpParser]
tokenize_helper [in ImpParser]
transitive [in Rel]
trans_eq_example' [in ProofObjects]
trans_eq_exercise [in MoreCoq]
trans_eq_example' [in MoreCoq]
trans_eq_example [in MoreCoq]
true_for_all_numbers [in Prop]
true_for_zero [in Prop]

U

update [in Imp]

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]

Global Index

other

(2764 entries)

Notation Index

other

(188 entries)

Module Index

other

(71 entries)

Variable Index

other

(8 entries)

Library Index

other

(39 entries)

Lemma Index

other

(741 entries)

Constructor Index

other

(848 entries)

Axiom Index

other

(12 entries)

Inductive Index

other

(187 entries)

Section Index

other

(4 entries)

Abbreviation Index

other

(55 entries)

Definition Index

other

(611 entries)

This page has been generated by coqdoc