| Global Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | : | _ | (2854 entries) |
| Notation Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | : | _ | (174 entries) |
| Module Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | (81 entries) | |
| Variable Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | (8 entries) | |
| Library Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | (40 entries) | |
| Constructor Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | (854 entries) | |
| Lemma Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | (767 entries) | |
| Axiom Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | (12 entries) | |
| Inductive Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | (184 entries) | |
| Section Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | (3 entries) | |
| Abbreviation Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | (55 entries) | |
| Definition Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | (676 entries) |
Global Index
A
abs_arrow [lemma, in Top.Sub]abs_arrow [lemma, in Top.RecordSub]
add1 [definition, in Top.ProofObjects]
admit [definition, in Top.SfLib]
admit [definition, in Top.Basics]
aequiv [definition, in Top.Equiv]
aequiv_example [lemma, in Top.Equiv]
aeval [definition, in Top.Imp]
aevalR_division [module, in Top.Imp]
aevalR_division.ADiv [constructor, in Top.Imp]
aevalR_division.aevalR [inductive, in Top.Imp]
aevalR_division.aexp [inductive, in Top.Imp]
aevalR_division.AMinus [constructor, in Top.Imp]
aevalR_division.AMult [constructor, in Top.Imp]
aevalR_division.ANum [constructor, in Top.Imp]
aevalR_division.APlus [constructor, in Top.Imp]
aevalR_division.E_ADiv [constructor, in Top.Imp]
aevalR_division.E_AMinus [constructor, in Top.Imp]
aevalR_division.E_AMult [constructor, in Top.Imp]
aevalR_division.E_ANum [constructor, in Top.Imp]
aevalR_division.E_APlus [constructor, in Top.Imp]
aevalR_division.:type_scope:x_'\\'_x [notation, in Top.Imp]
aevalR_extended [module, in Top.Imp]
aevalR_extended.AAny [constructor, in Top.Imp]
aevalR_extended.aevalR [inductive, in Top.Imp]
aevalR_extended.aexp [inductive, in Top.Imp]
aevalR_extended.AMinus [constructor, in Top.Imp]
aevalR_extended.AMult [constructor, in Top.Imp]
aevalR_extended.ANum [constructor, in Top.Imp]
aevalR_extended.APlus [constructor, in Top.Imp]
aevalR_extended.E_AMinus [constructor, in Top.Imp]
aevalR_extended.E_AMult [constructor, in Top.Imp]
aevalR_extended.E_ANum [constructor, in Top.Imp]
aevalR_extended.E_Any [constructor, in Top.Imp]
aevalR_extended.E_APlus [constructor, in Top.Imp]
aevalR_extended.:type_scope:x_'\\'_x [notation, in Top.Imp]
aeval_weakening [lemma, in Top.Equiv]
aexp [inductive, in Top.Imp]
AExp [module, in Top.Imp]
AExp.aeval [definition, in Top.Imp]
AExp.aevalR [inductive, in Top.Imp]
AExp.aevalR_first_try [module, in Top.Imp]
AExp.aevalR_first_try.aevalR [inductive, in Top.Imp]
AExp.aevalR_first_try.E_AMinus [constructor, in Top.Imp]
AExp.aevalR_first_try.E_AMult [constructor, in Top.Imp]
AExp.aevalR_first_try.E_ANum [constructor, in Top.Imp]
AExp.aevalR_first_try.E_APlus [constructor, in Top.Imp]
AExp.aevalR_first_try.:type_scope:x_'\\'_x [notation, in Top.Imp]
AExp.aeval_iff_aevalR [lemma, in Top.Imp]
AExp.aeval_iff_aevalR' [lemma, in Top.Imp]
AExp.aexp [inductive, in Top.Imp]
AExp.AMinus [constructor, in Top.Imp]
AExp.AMult [constructor, in Top.Imp]
AExp.ANum [constructor, in Top.Imp]
AExp.APlus [constructor, in Top.Imp]
AExp.BAnd [constructor, in Top.Imp]
AExp.BEq [constructor, in Top.Imp]
AExp.beval [definition, in Top.Imp]
AExp.bexp [inductive, in Top.Imp]
AExp.BFalse [constructor, in Top.Imp]
AExp.BLe [constructor, in Top.Imp]
AExp.BNot [constructor, in Top.Imp]
AExp.BTrue [constructor, in Top.Imp]
AExp.E_AMinus [constructor, in Top.Imp]
AExp.E_AMult [constructor, in Top.Imp]
AExp.E_ANum [constructor, in Top.Imp]
AExp.E_APlus [constructor, in Top.Imp]
AExp.foo [lemma, in Top.Imp]
AExp.foo' [lemma, in Top.Imp]
AExp.In10 [lemma, in Top.Imp]
AExp.In10' [lemma, in Top.Imp]
AExp.optimize_0plus [definition, in Top.Imp]
AExp.optimize_0plus_b [definition, in Top.Imp]
AExp.optimize_0plus_b_sound [lemma, in Top.Imp]
AExp.optimize_0plus_sound [lemma, in Top.Imp]
AExp.optimize_0plus_sound' [lemma, in Top.Imp]
AExp.optimize_0plus_sound'' [lemma, in Top.Imp]
AExp.silly1 [lemma, in Top.Imp]
AExp.silly2 [lemma, in Top.Imp]
AExp.silly_presburger_example [definition, in Top.Imp]
AExp.test_aeval1 [definition, in Top.Imp]
AExp.test_optimize_0plus [definition, in Top.Imp]
AExp.:type_scope:x_'\\'_x [notation, in Top.Imp]
aexp1 [definition, in Top.Imp]
afi_abs [constructor, in Top.RecordSub]
afi_abs [constructor, in Top.Norm]
afi_abs [constructor, in Top.Sub]
afi_app1 [constructor, in Top.RecordSub]
afi_app1 [constructor, in Top.Norm]
afi_app1 [constructor, in Top.Sub]
afi_app2 [constructor, in Top.RecordSub]
afi_app2 [constructor, in Top.Sub]
afi_app2 [constructor, in Top.Norm]
afi_fst [constructor, in Top.Norm]
afi_if0 [constructor, in Top.Norm]
afi_if1 [constructor, in Top.Sub]
afi_if1 [constructor, in Top.Norm]
afi_if2 [constructor, in Top.Norm]
afi_if2 [constructor, in Top.Sub]
afi_if3 [constructor, in Top.Sub]
afi_pair1 [constructor, in Top.Norm]
afi_pair2 [constructor, in Top.Norm]
afi_proj [constructor, in Top.RecordSub]
afi_rhead [constructor, in Top.RecordSub]
afi_rtail [constructor, in Top.RecordSub]
afi_snd [constructor, in Top.Norm]
afi_var [constructor, in Top.Norm]
afi_var [constructor, in Top.Sub]
afi_var [constructor, in Top.RecordSub]
AId [constructor, in Top.Imp]
All [definition, in Top.Logic]
all3_spec [lemma, in Top.Induction]
All_In [lemma, in Top.Logic]
alpha [constructor, in Top.ImpParser]
always_loop_hoare [lemma, in Top.Hoare]
AMinus [constructor, in Top.Imp]
AMult [constructor, in Top.Imp]
andb [definition, in Top.Basics]
andb3 [definition, in Top.Basics]
andb3_exchange [lemma, in Top.Basics]
andb_commutative [lemma, in Top.Basics]
andb_commutative' [lemma, in Top.Basics]
andb_commutative'' [lemma, in Top.Basics]
andb_eq_orb [lemma, in Top.Basics]
andb_false_r [lemma, in Top.Induction]
andb_true_elim2 [lemma, in Top.Basics]
andb_true_iff [lemma, in Top.Logic]
and_assoc [lemma, in Top.Logic]
and_commut [lemma, in Top.Logic]
and_example [definition, in Top.Logic]
and_example' [definition, in Top.Logic]
and_example2 [lemma, in Top.Logic]
and_example2' [lemma, in Top.Logic]
and_example2'' [lemma, in Top.Logic]
and_example3 [lemma, in Top.Logic]
and_exercise [definition, in Top.Logic]
and_intro [lemma, in Top.Logic]
antisymmetric [definition, in Top.Rel]
ANum [constructor, in Top.Imp]
APlus [constructor, in Top.Imp]
App [constructor, in Top.IndProp]
app [definition, in Top.Poly]
appears_free_in [inductive, in Top.Norm]
appears_free_in [inductive, in Top.Sub]
appears_free_in [inductive, in Top.RecordSub]
apply_iff_example [lemma, in Top.Logic]
app_assoc [lemma, in Top.Poly]
app_length [lemma, in Top.Poly]
app_length_cons [lemma, in Top.Tactics]
app_length_twice [lemma, in Top.Tactics]
app_nil_r [lemma, in Top.Poly]
Assertion [definition, in Top.Hoare]
assert_implies [definition, in Top.Hoare]
Assign [constructor, in Top.PE]
assign [definition, in Top.PE]
assigned [definition, in Top.PE]
assign_aequiv [lemma, in Top.Equiv]
assign_removes [lemma, in Top.PE]
assn_sub [definition, in Top.Hoare]
assn_sub_example [definition, in Top.Hoare]
astep [inductive, in Top.Smallstep]
astep_example1 [definition, in Top.Types]
astep_example1' [definition, in Top.Types]
astep_example1'' [definition, in Top.Types]
astep_example1''' [definition, in Top.Types]
AS_Id [constructor, in Top.Smallstep]
AS_Minus [constructor, in Top.Smallstep]
AS_Minus1 [constructor, in Top.Smallstep]
AS_Minus2 [constructor, in Top.Smallstep]
AS_Mult [constructor, in Top.Smallstep]
AS_Mult1 [constructor, in Top.Smallstep]
AS_Mult2 [constructor, in Top.Smallstep]
AS_Plus [constructor, in Top.Smallstep]
AS_Plus1 [constructor, in Top.Smallstep]
AS_Plus2 [constructor, in Top.Smallstep]
atrans_sound [definition, in Top.Equiv]
Auto [library]
auto_example_1 [definition, in Top.Auto]
auto_example_1' [definition, in Top.Auto]
auto_example_2 [definition, in Top.Auto]
auto_example_3 [definition, in Top.Auto]
auto_example_4 [definition, in Top.Auto]
auto_example_5 [definition, in Top.Auto]
auto_example_6 [definition, in Top.Auto]
auto_example_6' [definition, in Top.Auto]
auto_example_7 [definition, in Top.Auto]
auto_example_7' [definition, in Top.Auto]
auto_example_8 [definition, in Top.Auto]
auto_example_8' [definition, in Top.Auto]
aval [inductive, in Top.Smallstep]
av_num [constructor, in Top.Smallstep]
B
BAnd [constructor, in Top.Imp]bar [definition, in Top.Tactics]
Basics [library]
bassn [definition, in Top.Hoare]
bassn_eval_false [lemma, in Top.HoareAsLogic]
baz [inductive, in Top.Lists]
Baz1 [constructor, in Top.Lists]
Baz2 [constructor, in Top.Lists]
bempty [constructor, in Top.IndPrinciples]
BEq [constructor, in Top.Imp]
bequiv [definition, in Top.Equiv]
bequiv_example [lemma, in Top.Equiv]
beq_id [definition, in Top.Maps]
beq_id [definition, in Top.Lists]
beq_idP [lemma, in Top.Maps]
beq_id_false_iff [lemma, in Top.Maps]
beq_id_refl [lemma, in Top.Lists]
beq_id_refl [lemma, in Top.Maps]
beq_id_true [lemma, in Top.Tactics]
beq_id_true_iff [lemma, in Top.Maps]
beq_list [definition, in Top.Logic]
beq_list_true_iff [lemma, in Top.Logic]
beq_nat [definition, in Top.Basics]
beq_natP [lemma, in Top.IndProp]
beq_nat_false_iff [lemma, in Top.Logic]
beq_nat_refl [lemma, in Top.Induction]
beq_nat_sym [lemma, in Top.Tactics]
beq_nat_trans [lemma, in Top.Tactics]
beq_nat_true [lemma, in Top.Tactics]
beq_nat_true_iff [lemma, in Top.Logic]
beq_nat_0_l [lemma, in Top.Tactics]
beval [definition, in Top.Imp]
bexp [inductive, in Top.Imp]
bexp1 [definition, in Top.Imp]
bexp_eval_false [lemma, in Top.Hoare]
bexp_eval_true [lemma, in Top.Hoare]
BFalse [constructor, in Top.Imp]
Bib [library]
bignumber [definition, in Top.ImpParser]
BLe [constructor, in Top.Imp]
bleaf [constructor, in Top.IndPrinciples]
block [inductive, in Top.PE]
blt_nat [definition, in Top.Basics]
blue [constructor, in Top.IndPrinciples]
BNot [constructor, in Top.Imp]
body [constructor, in Top.PE]
bool [inductive, in Top.Basics]
boollist [inductive, in Top.Poly]
bool_canonical [lemma, in Top.Types]
bool_cons [constructor, in Top.Poly]
bool_fn_applied_thrice [lemma, in Top.Tactics]
bool_nil [constructor, in Top.Poly]
Boxer [inductive, in Top.LibTactics]
boxer [constructor, in Top.LibTactics]
BreakImp [module, in Top.Imp]
BreakImp.break_ignore [lemma, in Top.Imp]
BreakImp.CAss [constructor, in Top.Imp]
BreakImp.CBreak [constructor, in Top.Imp]
BreakImp.ceval [inductive, in Top.Imp]
BreakImp.ceval_deterministic [lemma, in Top.Imp]
BreakImp.CIf [constructor, in Top.Imp]
BreakImp.com [inductive, in Top.Imp]
BreakImp.CSeq [constructor, in Top.Imp]
BreakImp.CSkip [constructor, in Top.Imp]
BreakImp.CWhile [constructor, in Top.Imp]
BreakImp.E_Skip [constructor, in Top.Imp]
BreakImp.SBreak [constructor, in Top.Imp]
BreakImp.SContinue [constructor, in Top.Imp]
BreakImp.status [inductive, in Top.Imp]
BreakImp.while_break_true [lemma, in Top.Imp]
BreakImp.while_continue [lemma, in Top.Imp]
BreakImp.while_stops_on_break [lemma, in Top.Imp]
BreakImp.::x_'/'_x_'\\'_x_'/'_x [notation, in Top.Imp]
BreakImp.::x_'::='_x [notation, in Top.Imp]
BreakImp.::x_';;'_x [notation, in Top.Imp]
BreakImp.::'BREAK' [notation, in Top.Imp]
BreakImp.::'IFB'_x_'THEN'_x_'ELSE'_x_'FI' [notation, in Top.Imp]
BreakImp.::'SKIP' [notation, in Top.Imp]
BreakImp.::'WHILE'_x_'DO'_x_'END' [notation, in Top.Imp]
bstep [inductive, in Top.Smallstep]
BS_AndFalse [constructor, in Top.Smallstep]
BS_AndStep [constructor, in Top.Smallstep]
BS_AndTrueFalse [constructor, in Top.Smallstep]
BS_AndTrueStep [constructor, in Top.Smallstep]
BS_AndTrueTrue [constructor, in Top.Smallstep]
BS_Eq [constructor, in Top.Smallstep]
BS_Eq1 [constructor, in Top.Smallstep]
BS_Eq2 [constructor, in Top.Smallstep]
BS_LtEq [constructor, in Top.Smallstep]
BS_LtEq1 [constructor, in Top.Smallstep]
BS_LtEq2 [constructor, in Top.Smallstep]
BS_NotFalse [constructor, in Top.Smallstep]
BS_NotStep [constructor, in Top.Smallstep]
BS_NotTrue [constructor, in Top.Smallstep]
btrans_sound [definition, in Top.Equiv]
BTrue [constructor, in Top.Imp]
build_symtable [definition, in Top.ImpParser]
bvalue [inductive, in Top.Types]
bv_false [constructor, in Top.Types]
bv_true [constructor, in Top.Types]
byntree [inductive, in Top.IndPrinciples]
C
C [constructor, in Top.Smallstep]canonical_forms_of_arrow_types [lemma, in Top.RecordSub]
canonical_forms_of_arrow_types [lemma, in Top.Sub]
canonical_forms_of_Bool [lemma, in Top.Sub]
capprox [definition, in Top.Equiv]
CAss [constructor, in Top.Imp]
CAss_congruence [lemma, in Top.Equiv]
cequiv [definition, in Top.Equiv]
ceval [inductive, in Top.Imp]
ceval_and_ceval_step_coincide [lemma, in Top.ImpCEvalFun]
ceval_deterministic [lemma, in Top.Imp]
ceval_deterministic [lemma, in Top.Auto]
ceval_deterministic' [lemma, in Top.Auto]
ceval_deterministic' [lemma, in Top.ImpCEvalFun]
ceval_deterministic'' [lemma, in Top.Auto]
ceval_deterministic''' [lemma, in Top.Auto]
ceval_deterministic'''' [lemma, in Top.Auto]
ceval_deterministic''''' [lemma, in Top.Auto]
ceval_deterministic'_alt [lemma, in Top.Auto]
ceval_example1 [definition, in Top.Imp]
ceval_example2 [definition, in Top.Imp]
ceval_extensionality [lemma, in Top.PE]
ceval_fun_no_while [definition, in Top.Imp]
ceval_step [definition, in Top.ImpCEvalFun]
ceval_step1 [definition, in Top.ImpCEvalFun]
ceval_step2 [definition, in Top.ImpCEvalFun]
ceval_step3 [definition, in Top.ImpCEvalFun]
ceval_step_more [lemma, in Top.ImpCEvalFun]
ceval_step__ceval [lemma, in Top.ImpCEvalFun]
ceval__ceval_step [lemma, in Top.ImpCEvalFun]
Char [constructor, in Top.IndProp]
chartype [inductive, in Top.ImpParser]
CIf [constructor, in Top.Imp]
CIf_congruence [lemma, in Top.Equiv]
CImp [module, in Top.Smallstep]
CImp.CAss [constructor, in Top.Smallstep]
CImp.CIf [constructor, in Top.Smallstep]
CImp.cmultistep [definition, in Top.Smallstep]
CImp.com [inductive, in Top.Smallstep]
CImp.CPar [constructor, in Top.Smallstep]
CImp.CSeq [constructor, in Top.Smallstep]
CImp.CSkip [constructor, in Top.Smallstep]
CImp.cstep [inductive, in Top.Smallstep]
CImp.CS_Ass [constructor, in Top.Smallstep]
CImp.CS_AssStep [constructor, in Top.Smallstep]
CImp.CS_IfFalse [constructor, in Top.Smallstep]
CImp.CS_IfStep [constructor, in Top.Smallstep]
CImp.CS_IfTrue [constructor, in Top.Smallstep]
CImp.CS_ParDone [constructor, in Top.Smallstep]
CImp.CS_Par1 [constructor, in Top.Smallstep]
CImp.CS_Par2 [constructor, in Top.Smallstep]
CImp.CS_SeqFinish [constructor, in Top.Smallstep]
CImp.CS_SeqStep [constructor, in Top.Smallstep]
CImp.CS_While [constructor, in Top.Smallstep]
CImp.CWhile [constructor, in Top.Smallstep]
CImp.par_body_n [lemma, in Top.Smallstep]
CImp.par_body_n__Sn [lemma, in Top.Smallstep]
CImp.par_loop [definition, in Top.Smallstep]
CImp.par_loop_any_X [lemma, in Top.Smallstep]
CImp.par_loop_example_0 [definition, in Top.Smallstep]
CImp.par_loop_example_2 [definition, in Top.Smallstep]
CImp.::x_'/'_x_'==>'_x_'/'_x [notation, in Top.Smallstep]
CImp.::x_'/'_x_'==>*'_x_'/'_x [notation, in Top.Smallstep]
CImp.::x_'::='_x [notation, in Top.Smallstep]
CImp.::x_';;'_x [notation, in Top.Smallstep]
CImp.::'IFB'_x_'THEN'_x_'ELSE'_x_'FI' [notation, in Top.Smallstep]
CImp.::'PAR'_x_'WITH'_x_'END' [notation, in Top.Smallstep]
CImp.::'SKIP' [notation, in Top.Smallstep]
CImp.::'WHILE'_x_'DO'_x_'END' [notation, in Top.Smallstep]
classifyChar [definition, in Top.ImpParser]
closed [definition, in Top.Norm]
closed_env [definition, in Top.Norm]
clos_refl_trans [inductive, in Top.Rel]
clos_refl_trans_1n [inductive, in Top.Rel]
cmin [definition, in Top.Equiv]
cmin_minimal [lemma, in Top.Equiv]
COIND [definition, in Top.LibTactics]
com [inductive, in Top.Imp]
combine [definition, in Top.Poly]
Combined [module, in Top.Smallstep]
Combined.C [constructor, in Top.Smallstep]
Combined.P [constructor, in Top.Smallstep]
Combined.step [inductive, in Top.Smallstep]
Combined.ST_If [constructor, in Top.Smallstep]
Combined.ST_IfFalse [constructor, in Top.Smallstep]
Combined.ST_IfTrue [constructor, in Top.Smallstep]
Combined.ST_PlusConstConst [constructor, in Top.Smallstep]
Combined.ST_Plus1 [constructor, in Top.Smallstep]
Combined.ST_Plus2 [constructor, in Top.Smallstep]
Combined.tfalse [constructor, in Top.Smallstep]
Combined.tif [constructor, in Top.Smallstep]
Combined.tm [inductive, in Top.Smallstep]
Combined.ttrue [constructor, in Top.Smallstep]
Combined.value [inductive, in Top.Smallstep]
Combined.v_const [constructor, in Top.Smallstep]
Combined.v_false [constructor, in Top.Smallstep]
Combined.v_true [constructor, in Top.Smallstep]
Combined.::x_'==>'_x [notation, in Top.Smallstep]
combine_odd_even [definition, in Top.Logic]
combine_odd_even_elim_even [lemma, in Top.Logic]
combine_odd_even_elim_odd [lemma, in Top.Logic]
combine_odd_even_intro [lemma, in Top.Logic]
combine_split [lemma, in Top.Tactics]
compiler_is_correct [lemma, in Top.Smallstep]
compiler_is_correct_statement [definition, in Top.Smallstep]
congruence_demo_1 [lemma, in Top.UseAuto]
congruence_demo_2 [lemma, in Top.UseAuto]
congruence_demo_3 [lemma, in Top.UseAuto]
congruence_demo_4 [lemma, in Top.UseAuto]
congruence_example [definition, in Top.Equiv]
cons [constructor, in Top.Poly]
constfun [definition, in Top.Poly]
constfun_example1 [definition, in Top.Poly]
constfun_example2 [definition, in Top.Poly]
cons' [constructor, in Top.Poly]
context [definition, in Top.Norm]
context [definition, in Top.RecordSub]
context [definition, in Top.Sub]
context_invariance [lemma, in Top.RecordSub]
context_invariance [lemma, in Top.Norm]
context_invariance [lemma, in Top.Sub]
contradiction_implies_anything [lemma, in Top.Logic]
contrapositive [lemma, in Top.Logic]
countoddmembers' [definition, in Top.Poly]
CSeq [constructor, in Top.Imp]
CSeq_congruence [lemma, in Top.Equiv]
CSkip [constructor, in Top.Imp]
cstep [inductive, in Top.Smallstep]
CS_Ass [constructor, in Top.Smallstep]
CS_AssStep [constructor, in Top.Smallstep]
CS_IfFalse [constructor, in Top.Smallstep]
CS_IfStep [constructor, in Top.Smallstep]
CS_IfTrue [constructor, in Top.Smallstep]
CS_SeqFinish [constructor, in Top.Smallstep]
CS_SeqStep [constructor, in Top.Smallstep]
CS_While [constructor, in Top.Smallstep]
ctrans_sound [definition, in Top.Equiv]
CWhile [constructor, in Top.Imp]
CWhile_congruence [lemma, in Top.Equiv]
C1 [constructor, in Top.IndPrinciples]
C2 [constructor, in Top.IndPrinciples]
c3 [definition, in Top.Equiv]
c3_c4_different [lemma, in Top.Equiv]
c4 [definition, in Top.Equiv]
D
day [inductive, in Top.Basics]DCAsgn [constructor, in Top.Hoare2]
DCIf [constructor, in Top.Hoare2]
dcom [inductive, in Top.Hoare2]
DCPost [constructor, in Top.Hoare2]
DCPre [constructor, in Top.Hoare2]
DCSeq [constructor, in Top.Hoare2]
DCSkip [constructor, in Top.Hoare2]
DCWhile [constructor, in Top.Hoare2]
dec_correct [definition, in Top.Hoare2]
dec_while [definition, in Top.Hoare2]
dec_while_correct [lemma, in Top.Hoare2]
DemoAbsurd1 [section, in Top.UseAuto]
demo_auto_absurd_1 [lemma, in Top.UseAuto]
demo_auto_absurd_2 [lemma, in Top.UseAuto]
demo_clears_all_and_clears_but [lemma, in Top.LibTactics]
demo_false [lemma, in Top.UseTactics]
demo_false [lemma, in Top.UseAuto]
demo_false_arg [lemma, in Top.UseTactics]
demo_hint_unfold_context_1 [lemma, in Top.UseAuto]
demo_hint_unfold_context_2 [lemma, in Top.UseAuto]
demo_hint_unfold_goal_1 [lemma, in Top.UseAuto]
demo_hint_unfold_goal_2 [lemma, in Top.UseAuto]
demo_tryfalse [lemma, in Top.UseTactics]
deterministic [definition, in Top.Smallstep]
DeterministicImp [module, in Top.UseAuto]
DeterministicImp.ceval_deterministic [lemma, in Top.UseAuto]
DeterministicImp.ceval_deterministic' [lemma, in Top.UseAuto]
DeterministicImp.ceval_deterministic'' [lemma, in Top.UseAuto]
DeterministicImp.ceval_deterministic''' [lemma, in Top.UseAuto]
DeterministicImp.ceval_deterministic'''' [lemma, in Top.UseAuto]
de_morgan_not_and_not [definition, in Top.Logic]
digit [constructor, in Top.ImpParser]
dist_exists_or [lemma, in Top.Logic]
dist_not_exists [lemma, in Top.Logic]
div_mod_dec [definition, in Top.Hoare2]
div_mod_dec_correct [lemma, in Top.Hoare2]
doit3times [definition, in Top.Poly]
done [constructor, in Top.PE]
double [definition, in Top.Induction]
double_induction [lemma, in Top.Tactics]
double_injective [lemma, in Top.Tactics]
double_injective_FAILED [lemma, in Top.Tactics]
double_injective_take2 [lemma, in Top.Tactics]
double_injective_take2_FAILED [lemma, in Top.Tactics]
double_neg [lemma, in Top.Logic]
double_negation_elimination [definition, in Top.Logic]
double_plus [lemma, in Top.Induction]
dpow2_down [definition, in Top.Hoare2]
dpow2_down_correct [lemma, in Top.Hoare2]
drop [definition, in Top.Norm]
duplicate_subst [lemma, in Top.Norm]
dup_lemma [lemma, in Top.LibTactics]
E
empty [definition, in Top.Maps]EmptySet [constructor, in Top.IndProp]
EmptyStr [constructor, in Top.IndProp]
empty_is_empty [lemma, in Top.IndProp]
empty_pe_state [definition, in Top.PE]
empty_state [definition, in Top.Imp]
entry [constructor, in Top.PE]
env [definition, in Top.Norm]
EqualityExamples [module, in Top.UseTactics]
EqualityExamples.big_expression_using [axiom, in Top.UseTactics]
EqualityExamples.demo_applys_eq_1 [lemma, in Top.UseTactics]
EqualityExamples.demo_applys_eq_2 [lemma, in Top.UseTactics]
EqualityExamples.demo_applys_eq_3 [lemma, in Top.UseTactics]
EqualityExamples.demo_fequals [lemma, in Top.UseTactics]
EqualityExamples.demo_substs [lemma, in Top.UseTactics]
EqualityExamples.mult_0_plus [lemma, in Top.UseTactics]
EqualityExamples.mult_0_plus' [lemma, in Top.UseTactics]
EqualityExamples.mult_0_plus'' [lemma, in Top.UseTactics]
equality_by_auto [lemma, in Top.UseAuto]
equatesLemma [section, in Top.LibTactics]
equatesLemma.A0 [variable, in Top.LibTactics]
equatesLemma.A1 [variable, in Top.LibTactics]
equatesLemma.A2 [variable, in Top.LibTactics]
equatesLemma.A3 [variable, in Top.LibTactics]
equatesLemma.A4 [variable, in Top.LibTactics]
equatesLemma.A5 [variable, in Top.LibTactics]
equatesLemma.A6 [variable, in Top.LibTactics]
equates_0 [lemma, in Top.LibTactics]
equates_1 [lemma, in Top.LibTactics]
equates_2 [lemma, in Top.LibTactics]
equates_3 [lemma, in Top.LibTactics]
equates_4 [lemma, in Top.LibTactics]
equates_5 [lemma, in Top.LibTactics]
equates_6 [lemma, in Top.LibTactics]
Equiv [library]
equivalence [definition, in Top.Rel]
equiv_classes [definition, in Top.Equiv]
eq' [definition, in Top.LibTactics]
ev [inductive, in Top.IndProp]
ev [inductive, in Top.Hoare2]
eval [inductive, in Top.Smallstep]
evalF [definition, in Top.Smallstep]
evalF_eval [lemma, in Top.Smallstep]
eval_assign [lemma, in Top.PE]
eval__multistep [lemma, in Top.Smallstep]
evenb [definition, in Top.Basics]
evenb_double [lemma, in Top.Logic]
evenb_double_conv [lemma, in Top.Logic]
evenb_minus2 [lemma, in Top.IndProp]
evenb_S [lemma, in Top.Induction]
even5_nonsense [lemma, in Top.IndProp]
even_bool_prop [lemma, in Top.Logic]
even_1000 [definition, in Top.Logic]
even_1000' [definition, in Top.Logic]
even_1000'' [definition, in Top.Logic]
evSS_ev [lemma, in Top.IndProp]
evSS_ev [lemma, in Top.IndProp]
ev' [inductive, in Top.IndProp]
ev'_ev [lemma, in Top.IndProp]
ev'_sum [constructor, in Top.IndProp]
ev'_0 [constructor, in Top.IndProp]
ev'_2 [constructor, in Top.IndProp]
ev_double [lemma, in Top.IndProp]
ev_even [lemma, in Top.IndProp]
ev_even [lemma, in Top.IndProp]
ev_even_iff [lemma, in Top.IndProp]
ev_ev' [lemma, in Top.IndPrinciples]
ev_ev__ev [lemma, in Top.IndProp]
ev_minus2 [lemma, in Top.IndProp]
ev_minus2 [lemma, in Top.IndProp]
ev_minus2' [lemma, in Top.IndProp]
ev_plus2 [definition, in Top.ProofObjects]
ev_plus2' [definition, in Top.ProofObjects]
ev_plus2'' [definition, in Top.ProofObjects]
ev_plus4 [lemma, in Top.IndProp]
ev_plus4 [lemma, in Top.ProofObjects]
ev_plus4' [definition, in Top.ProofObjects]
ev_plus4'' [definition, in Top.ProofObjects]
ev_plus_plus [lemma, in Top.IndProp]
ev_SS [constructor, in Top.Hoare2]
ev_SS [constructor, in Top.IndProp]
ev_sum [lemma, in Top.IndProp]
ev_0 [constructor, in Top.IndProp]
ev_0 [constructor, in Top.Hoare2]
ev_4 [lemma, in Top.IndProp]
ev_4 [lemma, in Top.ProofObjects]
ev_4' [lemma, in Top.IndProp]
ev_4' [lemma, in Top.ProofObjects]
ev_4'' [lemma, in Top.ProofObjects]
ev_4''' [definition, in Top.ProofObjects]
ev_8 [lemma, in Top.ProofObjects]
ev_8' [definition, in Top.ProofObjects]
examplemap [definition, in Top.Maps]
Examples [module, in Top.RecordSub]
Examples [module, in Top.Sub]
ExamplesInstantiations [module, in Top.UseTactics]
ExamplesInstantiations.substitution_preserves_typing [lemma, in Top.UseTactics]
ExamplesLets [module, in Top.UseTactics]
ExamplesLets.demo_lets_underscore [lemma, in Top.UseTactics]
ExamplesLets.demo_lets_1 [lemma, in Top.UseTactics]
ExamplesLets.demo_lets_2 [lemma, in Top.UseTactics]
ExamplesLets.demo_lets_3 [lemma, in Top.UseTactics]
ExamplesLets.demo_lets_4 [lemma, in Top.UseTactics]
ExamplesLets.demo_lets_5 [lemma, in Top.UseTactics]
ExamplesLets.typing_inversion_var [axiom, in Top.UseTactics]
Examples.A [abbreviation, in Top.RecordSub]
Examples.A [abbreviation, in Top.Sub]
Examples.B [abbreviation, in Top.RecordSub]
Examples.B [abbreviation, in Top.Sub]
Examples.C [abbreviation, in Top.Sub]
Examples.C [abbreviation, in Top.RecordSub]
Examples.Employee [definition, in Top.Sub]
Examples.Float [abbreviation, in Top.Sub]
Examples.i [abbreviation, in Top.RecordSub]
Examples.Integer [abbreviation, in Top.Sub]
Examples.j [abbreviation, in Top.RecordSub]
Examples.k [abbreviation, in Top.RecordSub]
Examples.Person [definition, in Top.Sub]
Examples.String [abbreviation, in Top.Sub]
Examples.Student [definition, in Top.Sub]
Examples.subtyping_example_0 [definition, in Top.Sub]
Examples.subtyping_example_0 [definition, in Top.RecordSub]
Examples.subtyping_example_1 [definition, in Top.Sub]
Examples.subtyping_example_1 [definition, in Top.RecordSub]
Examples.subtyping_example_2 [definition, in Top.Sub]
Examples.subtyping_example_2 [definition, in Top.RecordSub]
Examples.subtyping_example_3 [definition, in Top.RecordSub]
Examples.subtyping_example_4 [definition, in Top.RecordSub]
Examples.sub_employee_person [definition, in Top.Sub]
Examples.sub_student_person [definition, in Top.Sub]
Examples.TRcd_j [definition, in Top.RecordSub]
Examples.TRcd_kj [definition, in Top.RecordSub]
Examples.x [abbreviation, in Top.RecordSub]
Examples.x [abbreviation, in Top.Sub]
Examples.y [abbreviation, in Top.Sub]
Examples.y [abbreviation, in Top.RecordSub]
Examples.z [abbreviation, in Top.RecordSub]
Examples.z [abbreviation, in Top.Sub]
Examples2 [module, in Top.RecordSub]
Examples2 [module, in Top.Sub]
Examples2.trcd_kj [definition, in Top.RecordSub]
Examples2.typing_example_0 [definition, in Top.RecordSub]
Examples2.typing_example_1 [definition, in Top.RecordSub]
Examples2.typing_example_2 [definition, in Top.RecordSub]
ExAssertions [module, in Top.Hoare]
ExAssertions.as1 [definition, in Top.Hoare]
ExAssertions.as2 [definition, in Top.Hoare]
ExAssertions.as3 [definition, in Top.Hoare]
ExAssertions.as4 [definition, in Top.Hoare]
ExAssertions.as5 [definition, in Top.Hoare]
ExAssertions.as6 [definition, in Top.Hoare]
excluded_middle [definition, in Top.Logic]
excluded_middle_irrefutable [lemma, in Top.Logic]
Exercises [module, in Top.Poly]
Exercises.Church [module, in Top.Poly]
Exercises.Church.exp [definition, in Top.Poly]
Exercises.Church.exp_1 [definition, in Top.Poly]
Exercises.Church.exp_2 [definition, in Top.Poly]
Exercises.Church.exp_3 [definition, in Top.Poly]
Exercises.Church.mult [definition, in Top.Poly]
Exercises.Church.mult_1 [definition, in Top.Poly]
Exercises.Church.mult_2 [definition, in Top.Poly]
Exercises.Church.mult_3 [definition, in Top.Poly]
Exercises.Church.nat [definition, in Top.Poly]
Exercises.Church.one [definition, in Top.Poly]
Exercises.Church.plus [definition, in Top.Poly]
Exercises.Church.plus_1 [definition, in Top.Poly]
Exercises.Church.plus_2 [definition, in Top.Poly]
Exercises.Church.plus_3 [definition, in Top.Poly]
Exercises.Church.succ [definition, in Top.Poly]
Exercises.Church.succ_1 [definition, in Top.Poly]
Exercises.Church.succ_2 [definition, in Top.Poly]
Exercises.Church.succ_3 [definition, in Top.Poly]
Exercises.Church.three [definition, in Top.Poly]
Exercises.Church.two [definition, in Top.Poly]
Exercises.Church.zero [definition, in Top.Poly]
Exercises.curry_uncurry [lemma, in Top.Poly]
Exercises.fold_length [definition, in Top.Poly]
Exercises.fold_length_correct [lemma, in Top.Poly]
Exercises.fold_map [definition, in Top.Poly]
Exercises.prod_curry [definition, in Top.Poly]
Exercises.prod_uncurry [definition, in Top.Poly]
Exercises.test_fold_length1 [definition, in Top.Poly]
Exercises.test_map2 [definition, in Top.Poly]
Exercises.uncurry_curry [lemma, in Top.Poly]
exists_example_2 [lemma, in Top.Logic]
exp [definition, in Top.Basics]
expect [definition, in Top.ImpParser]
exp_match [inductive, in Top.IndProp]
ExSet [inductive, in Top.IndPrinciples]
extract [definition, in Top.Hoare2]
Extraction [library]
ex_falso_quodlibet [lemma, in Top.Logic]
E_Ass [constructor, in Top.Imp]
E_Const [constructor, in Top.Smallstep]
E_IfFalse [constructor, in Top.Imp]
E_IfTrue [constructor, in Top.Imp]
E_None [constructor, in Top.PE]
E_Plus [constructor, in Top.Smallstep]
E_Seq [constructor, in Top.Imp]
E_Skip [constructor, in Top.Imp]
E_Some [constructor, in Top.PE]
E_WhileEnd [constructor, in Top.Imp]
E_WhileLoop [constructor, in Top.Imp]
F
factorial [definition, in Top.Basics]fact_in_coq [definition, in Top.Imp]
false [constructor, in Top.Basics]
False_and_P_imp [lemma, in Top.HoareAsLogic]
false_beq_id [lemma, in Top.Maps]
filter [definition, in Top.Poly]
filter_even_gt7 [definition, in Top.Poly]
filter_exercise [lemma, in Top.Tactics]
filter_not_empty_In [lemma, in Top.IndProp]
filter_not_empty_In' [lemma, in Top.IndProp]
find_parity [definition, in Top.Hoare2]
find_parity_correct [lemma, in Top.Hoare2]
find_parity_correct' [lemma, in Top.Hoare2]
find_parity_dec [definition, in Top.Hoare2]
find_parity_dec' [definition, in Top.Hoare2]
firstExpect [definition, in Top.ImpParser]
flat_map [definition, in Top.Poly]
fold [definition, in Top.Poly]
fold_aexp_ex1 [definition, in Top.Equiv]
fold_aexp_ex2 [definition, in Top.Equiv]
fold_bexp_ex1 [definition, in Top.Equiv]
fold_bexp_ex2 [definition, in Top.Equiv]
fold_com_ex1 [definition, in Top.Equiv]
fold_constants_aexp [definition, in Top.Equiv]
fold_constants_aexp_sound [lemma, in Top.Equiv]
fold_constants_bexp [definition, in Top.Equiv]
fold_constants_bexp_sound [lemma, in Top.Equiv]
fold_constants_com [definition, in Top.Equiv]
fold_constants_com_sound [lemma, in Top.Equiv]
fold_example1 [definition, in Top.Poly]
fold_example2 [definition, in Top.Poly]
fold_example3 [definition, in Top.Poly]
foo [definition, in Top.Tactics]
foo' [inductive, in Top.IndPrinciples]
forallb [definition, in Top.Logic]
forallb_true_iff [lemma, in Top.Logic]
four_is_even [lemma, in Top.Logic]
free_in_context [lemma, in Top.Sub]
free_in_context [lemma, in Top.RecordSub]
free_in_context [lemma, in Top.Norm]
friday [constructor, in Top.Basics]
fst [definition, in Top.Poly]
ftrue [definition, in Top.Poly]
functional_extensionality [axiom, in Top.Logic]
function_equality_ex [definition, in Top.Logic]
f_equal [lemma, in Top.Tactics]
G
GenExample [module, in Top.UseTactics]GenExample.substitution_preserves_typing [lemma, in Top.UseTactics]
Goto [constructor, in Top.PE]
green [constructor, in Top.IndPrinciples]
gt_not_le [axiom, in Top.UseAuto]
H
halts [definition, in Top.Norm]has_type [inductive, in Top.Sub]
has_type [inductive, in Top.Types]
has_type [inductive, in Top.Norm]
has_type [inductive, in Top.RecordSub]
has_type_not [definition, in Top.Types]
has_type_1 [definition, in Top.Types]
has_type__wf [lemma, in Top.RecordSub]
hd_error [definition, in Top.Poly]
Himp [module, in Top.Equiv]
Himp [module, in Top.Hoare]
Himp.CAsgn [constructor, in Top.Hoare]
Himp.CAss [constructor, in Top.Equiv]
Himp.cequiv [definition, in Top.Equiv]
Himp.ceval [inductive, in Top.Hoare]
Himp.ceval [inductive, in Top.Equiv]
Himp.CHavoc [constructor, in Top.Hoare]
Himp.CHavoc [constructor, in Top.Equiv]
Himp.CIf [constructor, in Top.Equiv]
Himp.CIf [constructor, in Top.Hoare]
Himp.com [inductive, in Top.Hoare]
Himp.com [inductive, in Top.Equiv]
Himp.CSeq [constructor, in Top.Hoare]
Himp.CSeq [constructor, in Top.Equiv]
Himp.CSkip [constructor, in Top.Equiv]
Himp.CSkip [constructor, in Top.Hoare]
Himp.CWhile [constructor, in Top.Hoare]
Himp.CWhile [constructor, in Top.Equiv]
Himp.E_Ass [constructor, in Top.Equiv]
Himp.E_Ass [constructor, in Top.Hoare]
Himp.E_Havoc [constructor, in Top.Hoare]
Himp.E_IfFalse [constructor, in Top.Equiv]
Himp.E_IfFalse [constructor, in Top.Hoare]
Himp.E_IfTrue [constructor, in Top.Equiv]
Himp.E_IfTrue [constructor, in Top.Hoare]
Himp.E_Seq [constructor, in Top.Hoare]
Himp.E_Seq [constructor, in Top.Equiv]
Himp.E_Skip [constructor, in Top.Equiv]
Himp.E_Skip [constructor, in Top.Hoare]
Himp.E_WhileEnd [constructor, in Top.Hoare]
Himp.E_WhileEnd [constructor, in Top.Equiv]
Himp.E_WhileLoop [constructor, in Top.Equiv]
Himp.E_WhileLoop [constructor, in Top.Hoare]
Himp.havoc_example1 [definition, in Top.Equiv]
Himp.havoc_example2 [definition, in Top.Equiv]
Himp.havoc_pre [definition, in Top.Hoare]
Himp.hoare_havoc [lemma, in Top.Hoare]
Himp.hoare_triple [definition, in Top.Hoare]
Himp.pcopy [definition, in Top.Equiv]
Himp.ptwice [definition, in Top.Equiv]
Himp.ptwice_cequiv_pcopy [lemma, in Top.Equiv]
Himp.pXY [definition, in Top.Equiv]
Himp.pXY_cequiv_pYX [lemma, in Top.Equiv]
Himp.pYX [definition, in Top.Equiv]
Himp.p1 [definition, in Top.Equiv]
Himp.p1_may_diverge [lemma, in Top.Equiv]
Himp.p1_p2_equiv [lemma, in Top.Equiv]
Himp.p2 [definition, in Top.Equiv]
Himp.p2_may_diverge [lemma, in Top.Equiv]
Himp.p3 [definition, in Top.Equiv]
Himp.p3_p4_inequiv [lemma, in Top.Equiv]
Himp.p4 [definition, in Top.Equiv]
Himp.p5 [definition, in Top.Equiv]
Himp.p5_p6_equiv [lemma, in Top.Equiv]
Himp.p6 [definition, in Top.Equiv]
{{'_x_'}}'_x_'{{'_x_'}}'">Himp.:hoare_spec_scope:'{{'_x_'}}'_x_'{{'_x_'}}' [notation, in Top.Hoare]
Himp.::x_'/'_x_'\\'_x [notation, in Top.Hoare]
Himp.::x_'/'_x_'\\'_x [notation, in Top.Equiv]
Himp.::x_'::='_x [notation, in Top.Hoare]
Himp.::x_'::='_x [notation, in Top.Equiv]
Himp.::x_';;'_x [notation, in Top.Hoare]
Himp.::x_';;'_x [notation, in Top.Equiv]
Himp.::'HAVOC'_x [notation, in Top.Hoare]
Himp.::'HAVOC'_x [notation, in Top.Equiv]
Himp.::'IFB'_x_'THEN'_x_'ELSE'_x_'FI' [notation, in Top.Hoare]
Himp.::'IFB'_x_'THEN'_x_'ELSE'_x_'FI' [notation, in Top.Equiv]
Himp.::'SKIP' [notation, in Top.Hoare]
Himp.::'SKIP' [notation, in Top.Equiv]
Himp.::'WHILE'_x_'DO'_x_'END' [notation, in Top.Equiv]
Himp.::'WHILE'_x_'DO'_x_'END' [notation, in Top.Hoare]
Himp2 [module, in Top.Hoare2]
Himp2.hoare_havoc_weakest [lemma, in Top.Hoare2]
HintsTransitivity [section, in Top.UseAuto]
Hoare [library]
HoareAsLogic [library]
Hoare2 [library]
hoare_asgn [lemma, in Top.Hoare]
hoare_asgn_example1 [definition, in Top.Hoare]
hoare_asgn_example1' [definition, in Top.Hoare]
hoare_asgn_example3 [definition, in Top.Hoare]
hoare_asgn_example4 [definition, in Top.Hoare]
hoare_asgn_fwd [lemma, in Top.Hoare]
hoare_asgn_fwd_exists [lemma, in Top.Hoare]
hoare_asgn_weakest [lemma, in Top.Hoare2]
hoare_consequence [lemma, in Top.Hoare]
hoare_consequence_post [lemma, in Top.Hoare]
hoare_consequence_pre [lemma, in Top.Hoare]
hoare_if [lemma, in Top.Hoare]
hoare_post_true [lemma, in Top.Hoare]
hoare_pre_false [lemma, in Top.Hoare]
hoare_proof [inductive, in Top.HoareAsLogic]
hoare_proof_complete [lemma, in Top.HoareAsLogic]
hoare_proof_sound [lemma, in Top.HoareAsLogic]
hoare_seq [lemma, in Top.Hoare]
hoare_skip [lemma, in Top.Hoare]
hoare_triple [definition, in Top.Hoare]
hoare_while [lemma, in Top.Hoare]
H_Asgn [constructor, in Top.HoareAsLogic]
H_Consequence [constructor, in Top.HoareAsLogic]
H_Consequence_post [lemma, in Top.HoareAsLogic]
H_Consequence_pre [lemma, in Top.HoareAsLogic]
H_If [constructor, in Top.HoareAsLogic]
H_Post_True_deriv [lemma, in Top.HoareAsLogic]
H_Pre_False_deriv [lemma, in Top.HoareAsLogic]
H_Seq [constructor, in Top.HoareAsLogic]
H_Skip [constructor, in Top.HoareAsLogic]
H_While [constructor, in Top.HoareAsLogic]
I
id [inductive, in Top.Lists]Id [constructor, in Top.Maps]
id [inductive, in Top.Maps]
Id [constructor, in Top.Lists]
identity_assignment [lemma, in Top.Equiv]
identity_fn_applied_twice [lemma, in Top.Basics]
If [constructor, in Top.PE]
IFB_false [lemma, in Top.Equiv]
IFB_true [lemma, in Top.Equiv]
IFB_true_simple [lemma, in Top.Equiv]
iff_intro_swap [lemma, in Top.LibTactics]
iff_refl [lemma, in Top.Logic]
iff_reflect [lemma, in Top.IndProp]
iff_sym [lemma, in Top.Logic]
iff_trans [lemma, in Top.Equiv]
iff_trans [lemma, in Top.Logic]
If1 [module, in Top.Hoare]
If1.CAss [constructor, in Top.Hoare]
If1.ceval [inductive, in Top.Hoare]
If1.CIf [constructor, in Top.Hoare]
If1.CIf1 [constructor, in Top.Hoare]
If1.com [inductive, in Top.Hoare]
If1.CSeq [constructor, in Top.Hoare]
If1.CSkip [constructor, in Top.Hoare]
If1.CWhile [constructor, in Top.Hoare]
If1.E_Ass [constructor, in Top.Hoare]
If1.E_IfFalse [constructor, in Top.Hoare]
If1.E_IfTrue [constructor, in Top.Hoare]
If1.E_Seq [constructor, in Top.Hoare]
If1.E_Skip [constructor, in Top.Hoare]
If1.E_WhileEnd [constructor, in Top.Hoare]
If1.E_WhileLoop [constructor, in Top.Hoare]
If1.hoare_if1_good [lemma, in Top.Hoare]
If1.hoare_triple [definition, in Top.Hoare]
{{'_x_'}}'_x_'{{'_x_'}}'">If1.:hoare_spec_scope:'{{'_x_'}}'_x_'{{'_x_'}}' [notation, in Top.Hoare]
If1.::x_'/'_x_'\\'_x [notation, in Top.Hoare]
If1.::x_'::='_x [notation, in Top.Hoare]
If1.::x_';;'_x [notation, in Top.Hoare]
If1.::'IFB'_x_'THEN'_x_'ELSE'_x_'FI' [notation, in Top.Hoare]
If1.::'IF1'_x_'THEN'_x_'FI' [notation, in Top.Hoare]
If1.::'SKIP' [notation, in Top.Hoare]
If1.::'WHILE'_x_'DO'_x_'END' [notation, in Top.Hoare]
if_example [definition, in Top.Hoare]
if_minus_correct [lemma, in Top.Hoare2]
if_minus_dec [definition, in Top.Hoare2]
if_minus_plus [lemma, in Top.Hoare]
if_minus_plus_com [definition, in Top.Hoare2]
if_minus_plus_correct [lemma, in Top.Hoare2]
if_minus_plus_dec [definition, in Top.Hoare2]
Imp [library]
ImpCEvalFun [library]
implies_to_or [definition, in Top.Logic]
ImpParser [library]
In [definition, in Top.Logic]
inb [definition, in Top.PE]
inbP [lemma, in Top.PE]
IndPrinciples [library]
IndProp [library]
Induction [library]
induct_height_max2 [lemma, in Top.LibTactics]
inequiv_exercise [lemma, in Top.Equiv]
injective [definition, in Top.Logic]
inj_pair2 [axiom, in Top.LibTactics]
instantiation [inductive, in Top.Norm]
instantiation_domains_match [lemma, in Top.Norm]
instantiation_drop [lemma, in Top.Norm]
instantiation_env_closed [lemma, in Top.Norm]
instantiation_R [lemma, in Top.Norm]
IntrovExamples [module, in Top.UseTactics]
IntrovExamples.ceval_deterministic [lemma, in Top.UseTactics]
IntrovExamples.ceval_deterministic' [lemma, in Top.UseTactics]
IntrovExamples.dist_exists_or [lemma, in Top.UseTactics]
IntrovExamples.exists_impl [lemma, in Top.UseTactics]
inversion_ex1 [lemma, in Top.Tactics]
inversion_ex2 [lemma, in Top.Tactics]
inversion_ex3 [definition, in Top.Tactics]
inversion_ex4 [lemma, in Top.Tactics]
inversion_ex5 [lemma, in Top.Tactics]
inversion_ex6 [definition, in Top.Tactics]
InvertsExamples [module, in Top.UseTactics]
InvertsExamples.ceval_deterministic [lemma, in Top.UseTactics]
InvertsExamples.ceval_deterministic' [lemma, in Top.UseTactics]
InvertsExamples.skip_left [lemma, in Top.UseTactics]
InvertsExamples.skip_left' [lemma, in Top.UseTactics]
InvertsExamples.typing_nonexample_1 [definition, in Top.UseTactics]
in_app_iff [lemma, in Top.Logic]
In_example_1 [definition, in Top.Logic]
In_example_2 [definition, in Top.Logic]
In_map [lemma, in Top.Logic]
In_map_iff [lemma, in Top.Logic]
in_re_match [lemma, in Top.IndProp]
in_split [lemma, in Top.IndProp]
isAlpha [definition, in Top.ImpParser]
isDigit [definition, in Top.ImpParser]
isLowerAlpha [definition, in Top.ImpParser]
isWhite [definition, in Top.ImpParser]
is_even_prime [definition, in Top.Logic]
is_fortytwo [definition, in Top.Auto]
is_three [definition, in Top.Logic]
is_wp [definition, in Top.Hoare2]
is_wp_example [lemma, in Top.Hoare2]
K
keval [definition, in Top.PE]keval_example [definition, in Top.PE]
L
le [inductive, in Top.IndPrinciples]leaf [constructor, in Top.IndPrinciples]
leb [definition, in Top.Basics]
leb_complete [lemma, in Top.IndProp]
leb_correct [lemma, in Top.IndProp]
leb_iff [lemma, in Top.IndProp]
leb_refl [lemma, in Top.Induction]
leb_true_trans [lemma, in Top.IndProp]
lemma_application_ex [definition, in Top.Logic]
LeModule [module, in Top.IndProp]
LeModule.le [inductive, in Top.IndProp]
LeModule.le_n [constructor, in Top.IndProp]
LeModule.le_S [constructor, in Top.IndProp]
LeModule.test_le1 [lemma, in Top.IndProp]
LeModule.test_le2 [lemma, in Top.IndProp]
LeModule.test_le3 [lemma, in Top.IndProp]
LeModule.::x_'<='_x [notation, in Top.IndProp]
length [definition, in Top.Poly]
length_is_1 [definition, in Top.Poly]
le_antisym [lemma, in Top.Auto]
le_antisymmetric [lemma, in Top.Rel]
le_gt_false [axiom, in Top.UseAuto]
le_n [constructor, in Top.IndPrinciples]
le_not_a_partial_function [lemma, in Top.Rel]
le_not_gt [axiom, in Top.UseAuto]
le_not_symmetric [lemma, in Top.Rel]
le_order [lemma, in Top.Rel]
le_plus_l [lemma, in Top.IndProp]
le_reflexive [lemma, in Top.Rel]
le_S [constructor, in Top.IndPrinciples]
le_Sn_le [lemma, in Top.Rel]
le_Sn_n [lemma, in Top.Rel]
le_step [lemma, in Top.Rel]
le_S_n [lemma, in Top.Rel]
le_trans [lemma, in Top.IndProp]
le_trans [lemma, in Top.Rel]
LibTactics [library]
LibTacticsCompatibility [module, in Top.LibTactics]
list [inductive, in Top.Poly]
Lists [library]
list' [inductive, in Top.Poly]
list123 [definition, in Top.Poly]
list123' [definition, in Top.Poly]
list123'' [definition, in Top.Poly]
list123''' [definition, in Top.Poly]
list_of_string [definition, in Top.ImpParser]
Logic [library]
lookup [definition, in Top.Norm]
lookup_field_in_value [lemma, in Top.RecordSub]
loop [constructor, in Top.PE]
loop [definition, in Top.Imp]
Loop [module, in Top.PE]
Loop.ceval_count [inductive, in Top.PE]
Loop.ceval_count_complete [lemma, in Top.PE]
Loop.ceval_count_sound [lemma, in Top.PE]
Loop.E'Ass [constructor, in Top.PE]
Loop.E'IfFalse [constructor, in Top.PE]
Loop.E'IfTrue [constructor, in Top.PE]
Loop.E'Seq [constructor, in Top.PE]
Loop.E'Skip [constructor, in Top.PE]
Loop.E'WhileEnd [constructor, in Top.PE]
Loop.E'WhileLoop [constructor, in Top.PE]
Loop.PE_AssDynamic [constructor, in Top.PE]
Loop.PE_AssStatic [constructor, in Top.PE]
Loop.pe_ceval_count [inductive, in Top.PE]
Loop.pe_ceval_count_intro [constructor, in Top.PE]
Loop.pe_ceval_count_le [lemma, in Top.PE]
Loop.pe_com [inductive, in Top.PE]
Loop.pe_compare_nil_lookup [lemma, in Top.PE]
Loop.pe_compare_nil_update [lemma, in Top.PE]
Loop.pe_com_complete [lemma, in Top.PE]
Loop.pe_com_correct [lemma, in Top.PE]
Loop.pe_com_sound [lemma, in Top.PE]
Loop.PE_If [constructor, in Top.PE]
Loop.PE_IfFalse [constructor, in Top.PE]
Loop.PE_IfTrue [constructor, in Top.PE]
Loop.pe_loop_example1 [definition, in Top.PE]
Loop.pe_loop_example2 [definition, in Top.PE]
Loop.pe_loop_example3 [definition, in Top.PE]
Loop.pe_loop_example4 [definition, in Top.PE]
Loop.PE_Seq [constructor, in Top.PE]
Loop.PE_Skip [constructor, in Top.PE]
Loop.PE_While [constructor, in Top.PE]
Loop.PE_WhileEnd [constructor, in Top.PE]
Loop.PE_WhileFixed [constructor, in Top.PE]
Loop.PE_WhileFixedEnd [constructor, in Top.PE]
Loop.PE_WhileFixedLoop [constructor, in Top.PE]
Loop.PE_WhileLoop [constructor, in Top.PE]
Loop.square_loop [definition, in Top.PE]
Loop.::x_'/'_x_'/'_x_'/'_x_'\\'_x_'#'_x [notation, in Top.PE]
Loop.::x_'/'_x_'\\'_x_'#'_x [notation, in Top.PE]
Loop.::x_'/'_x_'\\'_x_'/'_x_'/'_x [notation, in Top.PE]
loop_never_stops [lemma, in Top.Imp]
loop_unrolling [lemma, in Top.Equiv]
lt [definition, in Top.IndProp]
ltac_database [definition, in Top.LibTactics]
ltac_database_provide [lemma, in Top.LibTactics]
ltac_database_token [constructor, in Top.LibTactics]
Ltac_database_token [inductive, in Top.LibTactics]
ltac_mark [constructor, in Top.LibTactics]
ltac_Mark [inductive, in Top.LibTactics]
ltac_nat_from_int [definition, in Top.LibTactics]
ltac_no_arg [constructor, in Top.LibTactics]
ltac_No_arg [inductive, in Top.LibTactics]
ltac_something [definition, in Top.LibTactics]
ltac_something_eq [lemma, in Top.LibTactics]
ltac_something_hide [lemma, in Top.LibTactics]
ltac_something_show [lemma, in Top.LibTactics]
ltac_tag_subst [definition, in Top.LibTactics]
ltac_to_generalize [definition, in Top.LibTactics]
ltac_Wild [inductive, in Top.LibTactics]
ltac_wild [constructor, in Top.LibTactics]
ltac_Wilds [inductive, in Top.LibTactics]
ltac_wilds [constructor, in Top.LibTactics]
lt_S [lemma, in Top.IndProp]
lt_trans [lemma, in Top.Rel]
lt_trans' [lemma, in Top.Rel]
lt_trans'' [lemma, in Top.Rel]
l1 [lemma, in Top.Hoare2]
l2 [lemma, in Top.Hoare2]
l3 [lemma, in Top.Hoare2]
l3' [lemma, in Top.Hoare2]
l4 [lemma, in Top.Hoare2]
M
many [definition, in Top.ImpParser]many_helper [definition, in Top.ImpParser]
map [definition, in Top.Poly]
MApp [constructor, in Top.IndProp]
Maps [library]
map_rev [lemma, in Top.Poly]
MChar [constructor, in Top.IndProp]
MEmpty [constructor, in Top.IndProp]
minustwo [definition, in Top.Basics]
minus_diag [lemma, in Top.Induction]
monday [constructor, in Top.Basics]
MoreStlc [library]
MStarApp [constructor, in Top.IndProp]
MStar' [lemma, in Top.IndProp]
MStar'' [lemma, in Top.IndProp]
MStar0 [constructor, in Top.IndProp]
MStar1 [lemma, in Top.IndProp]
msubst [definition, in Top.Norm]
msubst_abs [lemma, in Top.Norm]
msubst_app [lemma, in Top.Norm]
msubst_closed [lemma, in Top.Norm]
msubst_preserves_typing [lemma, in Top.Norm]
msubst_R [lemma, in Top.Norm]
msubst_var [lemma, in Top.Norm]
multi [inductive, in Top.Smallstep]
multistep [abbreviation, in Top.Norm]
multistep [definition, in Top.Types]
multistep_App2 [lemma, in Top.Norm]
multistep_congr_1 [lemma, in Top.Smallstep]
multistep_congr_2 [lemma, in Top.Smallstep]
multistep_preserves_R [lemma, in Top.Norm]
multistep_preserves_R' [lemma, in Top.Norm]
multistep__eval [lemma, in Top.Smallstep]
multi_R [lemma, in Top.Smallstep]
multi_refl [constructor, in Top.Smallstep]
multi_step [constructor, in Top.Smallstep]
multi_trans [lemma, in Top.Smallstep]
mult_assoc [lemma, in Top.Induction]
mult_comm [lemma, in Top.Induction]
mult_eq_0 [lemma, in Top.Logic]
mult_plus_distr_r [lemma, in Top.Induction]
mult_S_1 [lemma, in Top.Basics]
mult_0 [lemma, in Top.Logic]
mult_0_l [lemma, in Top.Basics]
mult_0_plus [lemma, in Top.Basics]
mult_0_plus' [lemma, in Top.Induction]
mult_0_r [lemma, in Top.Induction]
mult_0_r' [lemma, in Top.IndPrinciples]
mult_0_r'' [lemma, in Top.IndPrinciples]
mult_0_3 [lemma, in Top.Logic]
mult_1_l [lemma, in Top.Induction]
MumbleGrumble [module, in Top.Poly]
MumbleGrumble.a [constructor, in Top.Poly]
MumbleGrumble.b [constructor, in Top.Poly]
MumbleGrumble.c [constructor, in Top.Poly]
MumbleGrumble.d [constructor, in Top.Poly]
MumbleGrumble.e [constructor, in Top.Poly]
MumbleGrumble.grumble [inductive, in Top.Poly]
MumbleGrumble.mumble [inductive, in Top.Poly]
MUnionL [constructor, in Top.IndProp]
MUnionR [constructor, in Top.IndProp]
MUnion' [lemma, in Top.IndProp]
mupdate [definition, in Top.Norm]
mupdate_drop [lemma, in Top.Norm]
mupdate_lookup [lemma, in Top.Norm]
MyEquality [module, in Top.ProofObjects]
MyEquality.eq [inductive, in Top.ProofObjects]
MyEquality.eq_refl [constructor, in Top.ProofObjects]
MyEquality.four [lemma, in Top.ProofObjects]
MyEquality.four' [definition, in Top.ProofObjects]
MyEquality.leibniz_equality [lemma, in Top.ProofObjects]
MyEquality.singleton [definition, in Top.ProofObjects]
MyEquality.:type_scope:x_'='_x [notation, in Top.ProofObjects]
myFact [definition, in Top.UseAuto]
MyIff [module, in Top.Logic]
MyIff.iff [definition, in Top.Logic]
MyIff.:type_scope:x_'<->'_x [notation, in Top.Logic]
mynil [definition, in Top.Poly]
mynil [definition, in Top.Poly]
mynil' [definition, in Top.Poly]
MyNot [module, in Top.Logic]
MyNot.not [definition, in Top.Logic]
MyNot.:type_scope:'~'_x [notation, in Top.Logic]
N
nandb [definition, in Top.Basics]NaryExamples [module, in Top.UseTactics]
NaryExamples.demo_branch [lemma, in Top.UseTactics]
NaryExamples.demo_splits [lemma, in Top.UseTactics]
NaryExamples.progress [lemma, in Top.UseTactics]
NatList [module, in Top.Lists]
natlist [inductive, in Top.IndPrinciples]
NatList.add [definition, in Top.Lists]
NatList.alternate [definition, in Top.Lists]
NatList.app [definition, in Top.Lists]
NatList.app_assoc [lemma, in Top.Lists]
NatList.app_assoc4 [lemma, in Top.Lists]
NatList.app_length [lemma, in Top.Lists]
NatList.app_nil_r [lemma, in Top.Lists]
NatList.bag [definition, in Top.Lists]
NatList.bag_theorem [lemma, in Top.Lists]
NatList.beq_natlist [definition, in Top.Lists]
NatList.beq_natlist_refl [lemma, in Top.Lists]
NatList.ble_n_Sn [lemma, in Top.Lists]
NatList.cons [constructor, in Top.Lists]
NatList.count [definition, in Top.Lists]
NatList.countoddmembers [definition, in Top.Lists]
NatList.count_member_nonzero [lemma, in Top.Lists]
NatList.fst [definition, in Top.Lists]
NatList.fst' [definition, in Top.Lists]
NatList.fst_swap_is_snd [lemma, in Top.Lists]
NatList.hd [definition, in Top.Lists]
NatList.hd_error [definition, in Top.Lists]
NatList.length [definition, in Top.Lists]
NatList.member [definition, in Top.Lists]
NatList.mylist [definition, in Top.Lists]
NatList.mylist1 [definition, in Top.Lists]
NatList.mylist2 [definition, in Top.Lists]
NatList.mylist3 [definition, in Top.Lists]
NatList.natlist [inductive, in Top.Lists]
NatList.natoption [inductive, in Top.Lists]
NatList.natprod [inductive, in Top.Lists]
NatList.nil [constructor, in Top.Lists]
NatList.nil_app [lemma, in Top.Lists]
NatList.None [constructor, in Top.Lists]
NatList.nonzeros [definition, in Top.Lists]
NatList.nonzeros_app [lemma, in Top.Lists]
NatList.nth_bad [definition, in Top.Lists]
NatList.nth_error [definition, in Top.Lists]
NatList.nth_error' [definition, in Top.Lists]
NatList.oddmembers [definition, in Top.Lists]
NatList.option_elim [definition, in Top.Lists]
NatList.option_elim_hd [lemma, in Top.Lists]
NatList.pair [constructor, in Top.Lists]
NatList.remove_all [definition, in Top.Lists]
NatList.remove_decreases_count [lemma, in Top.Lists]
NatList.remove_one [definition, in Top.Lists]
NatList.repeat [definition, in Top.Lists]
NatList.rev [definition, in Top.Lists]
NatList.rev_involutive [lemma, in Top.Lists]
NatList.rev_length [lemma, in Top.Lists]
NatList.rev_length_firsttry [lemma, in Top.Lists]
NatList.snd [definition, in Top.Lists]
NatList.snd' [definition, in Top.Lists]
NatList.snd_fst_is_swap [lemma, in Top.Lists]
NatList.Some [constructor, in Top.Lists]
NatList.subset [definition, in Top.Lists]
NatList.sum [definition, in Top.Lists]
NatList.surjective_pairing [lemma, in Top.Lists]
NatList.surjective_pairing' [lemma, in Top.Lists]
NatList.surjective_pairing_stuck [lemma, in Top.Lists]
NatList.swap_pair [definition, in Top.Lists]
NatList.test_add1 [definition, in Top.Lists]
NatList.test_add2 [definition, in Top.Lists]
NatList.test_alternate1 [definition, in Top.Lists]
NatList.test_alternate2 [definition, in Top.Lists]
NatList.test_alternate3 [definition, in Top.Lists]
NatList.test_alternate4 [definition, in Top.Lists]
NatList.test_app1 [definition, in Top.Lists]
NatList.test_app2 [definition, in Top.Lists]
NatList.test_app3 [definition, in Top.Lists]
NatList.test_beq_natlist1 [definition, in Top.Lists]
NatList.test_beq_natlist2 [definition, in Top.Lists]
NatList.test_beq_natlist3 [definition, in Top.Lists]
NatList.test_countoddmembers1 [definition, in Top.Lists]
NatList.test_countoddmembers2 [definition, in Top.Lists]
NatList.test_countoddmembers3 [definition, in Top.Lists]
NatList.test_count1 [definition, in Top.Lists]
NatList.test_count2 [definition, in Top.Lists]
NatList.test_hd1 [definition, in Top.Lists]
NatList.test_hd2 [definition, in Top.Lists]
NatList.test_hd_error1 [definition, in Top.Lists]
NatList.test_hd_error2 [definition, in Top.Lists]
NatList.test_hd_error3 [definition, in Top.Lists]
NatList.test_member1 [definition, in Top.Lists]
NatList.test_member2 [definition, in Top.Lists]
NatList.test_nonzeros [definition, in Top.Lists]
NatList.test_nth_error1 [definition, in Top.Lists]
NatList.test_nth_error2 [definition, in Top.Lists]
NatList.test_nth_error3 [definition, in Top.Lists]
NatList.test_oddmembers [definition, in Top.Lists]
NatList.test_remove_all1 [definition, in Top.Lists]
NatList.test_remove_all2 [definition, in Top.Lists]
NatList.test_remove_all3 [definition, in Top.Lists]
NatList.test_remove_all4 [definition, in Top.Lists]
NatList.test_remove_one1 [definition, in Top.Lists]
NatList.test_remove_one2 [definition, in Top.Lists]
NatList.test_remove_one3 [definition, in Top.Lists]
NatList.test_remove_one4 [definition, in Top.Lists]
NatList.test_rev1 [definition, in Top.Lists]
NatList.test_rev2 [definition, in Top.Lists]
NatList.test_subset1 [definition, in Top.Lists]
NatList.test_subset2 [definition, in Top.Lists]
NatList.test_sum1 [definition, in Top.Lists]
NatList.test_tl [definition, in Top.Lists]
NatList.tl [definition, in Top.Lists]
NatList.tl_length_pred [lemma, in Top.Lists]
NatList.::x_'++'_x [notation, in Top.Lists]
NatList.::x_'::'_x [notation, in Top.Lists]
NatList.::'('_x_','_x_')' [notation, in Top.Lists]
NatList.::'['_x_';'_'..'_';'_x_']' [notation, in Top.Lists]
NatList.::'['_']' [notation, in Top.Lists]
natlist1 [inductive, in Top.IndPrinciples]
nat_canonical [lemma, in Top.Types]
nbranch [constructor, in Top.IndPrinciples]
ncons [constructor, in Top.IndPrinciples]
negation_study_1 [lemma, in Top.UseAuto]
negation_study_2 [lemma, in Top.UseAuto]
negb [definition, in Top.Basics]
negb_involutive [lemma, in Top.Basics]
next_even [inductive, in Top.IndProp]
next_nat [inductive, in Top.IndProp]
next_nat_closure_is_le [lemma, in Top.Rel]
next_nat_partial_function [lemma, in Top.Rel]
next_weekday [definition, in Top.Basics]
ne_1 [constructor, in Top.IndProp]
ne_2 [constructor, in Top.IndProp]
nf_is_value [lemma, in Top.Smallstep]
nf_same_as_value [lemma, in Top.Smallstep]
nil [constructor, in Top.Poly]
nil' [constructor, in Top.Poly]
nn [constructor, in Top.IndProp]
nnil [constructor, in Top.IndPrinciples]
nnil1 [constructor, in Top.IndPrinciples]
no [constructor, in Top.IndPrinciples]
node [constructor, in Top.IndPrinciples]
None [constructor, in Top.Poly]
NoneE [constructor, in Top.ImpParser]
Norm [library]
normalization [lemma, in Top.Norm]
normalize_ex [lemma, in Top.Types]
normalize_ex' [lemma, in Top.Types]
normalizing [definition, in Top.Smallstep]
normal_form [definition, in Top.Smallstep]
normal_forms_unique [lemma, in Top.Smallstep]
normal_form_of [definition, in Top.Smallstep]
nostutter [inductive, in Top.IndProp]
not_both_true_and_false [lemma, in Top.Logic]
not_exists_dist [lemma, in Top.Logic]
not_False [lemma, in Top.Logic]
not_implies_our_not [lemma, in Top.Logic]
not_true_iff_false [lemma, in Top.Logic]
not_true_is_false [lemma, in Top.Logic]
not_true_is_false' [lemma, in Top.Logic]
no_whiles [definition, in Top.Imp]
no_whilesR [inductive, in Top.Imp]
no_whiles_eqv [lemma, in Top.Imp]
nsnoc1 [constructor, in Top.IndPrinciples]
nth_error [definition, in Top.Poly]
nth_error_after_last [lemma, in Top.Tactics]
nvalue [inductive, in Top.Types]
nv_succ [constructor, in Top.Types]
nv_zero [constructor, in Top.Types]
n_le_m__Sn_le_Sm [lemma, in Top.IndProp]
O
oddb [definition, in Top.Basics]omega_demo_1 [lemma, in Top.UseAuto]
omega_demo_2 [lemma, in Top.UseAuto]
omega_demo_3 [lemma, in Top.UseAuto]
omega_demo_4 [lemma, in Top.UseAuto]
one_not_even [lemma, in Top.IndProp]
option [inductive, in Top.Poly]
optionE [inductive, in Top.ImpParser]
option_map [definition, in Top.Poly]
orb [definition, in Top.Basics]
orb_true_iff [lemma, in Top.Logic]
order [definition, in Top.Rel]
order_matters_1 [lemma, in Top.UseAuto]
order_matters_2 [lemma, in Top.UseAuto]
or_assoc [lemma, in Top.Logic]
or_commut [lemma, in Top.Logic]
or_distributes_over_and [lemma, in Top.Logic]
or_example [lemma, in Top.Logic]
or_intro [lemma, in Top.Logic]
other [constructor, in Top.ImpParser]
O_le_n [lemma, in Top.IndProp]
P
P [axiom, in Top.UseAuto]P [constructor, in Top.Smallstep]
pair [constructor, in Top.Poly]
parity [definition, in Top.Hoare2]
parity [definition, in Top.PE]
parity_body [definition, in Top.PE]
parity_correct [lemma, in Top.Hoare2]
parity_dec [definition, in Top.Hoare2]
parity_dec_correct [lemma, in Top.Hoare2]
parity_eval [definition, in Top.PE]
parity_ge_2 [lemma, in Top.Hoare2]
parity_label [inductive, in Top.PE]
parity_lt_2 [lemma, in Top.Hoare2]
parse [definition, in Top.ImpParser]
parseAExp [definition, in Top.ImpParser]
parseAtomicExp [definition, in Top.ImpParser]
parseBExp [definition, in Top.ImpParser]
parseConjunctionExp [definition, in Top.ImpParser]
parseIdentifier [definition, in Top.ImpParser]
parseNumber [definition, in Top.ImpParser]
parsePrimaryExp [definition, in Top.ImpParser]
parseProductExp [definition, in Top.ImpParser]
parser [definition, in Top.ImpParser]
parseSequencedCommand [definition, in Top.ImpParser]
parseSimpleCommand [definition, in Top.ImpParser]
parseSumExp [definition, in Top.ImpParser]
PartialMap [module, in Top.Lists]
PartialMap.empty [constructor, in Top.Lists]
PartialMap.find [definition, in Top.Lists]
PartialMap.partial_map [inductive, in Top.Lists]
PartialMap.record [constructor, in Top.Lists]
PartialMap.update [definition, in Top.Lists]
PartialMap.update_eq [lemma, in Top.Lists]
PartialMap.update_neq [lemma, in Top.Lists]
partial_function [definition, in Top.Rel]
partial_map [definition, in Top.Maps]
partition [definition, in Top.Poly]
PE [library]
peirce [definition, in Top.Logic]
peval [inductive, in Top.PE]
pe_add [definition, in Top.PE]
pe_add_correct [lemma, in Top.PE]
pe_aexp [definition, in Top.PE]
pe_aexp_correct [lemma, in Top.PE]
pe_aexp_correct_weak [lemma, in Top.PE]
PE_AssDynamic [constructor, in Top.PE]
PE_AssStatic [constructor, in Top.PE]
pe_bexp [definition, in Top.PE]
pe_bexp_correct [lemma, in Top.PE]
pe_block [definition, in Top.PE]
pe_block_correct [lemma, in Top.PE]
pe_block_example [definition, in Top.PE]
pe_ceval [inductive, in Top.PE]
pe_ceval_intro [constructor, in Top.PE]
pe_com [inductive, in Top.PE]
pe_compare [definition, in Top.PE]
pe_compare_correct [lemma, in Top.PE]
pe_compare_removes [lemma, in Top.PE]
pe_compare_update [lemma, in Top.PE]
pe_com_complete [lemma, in Top.PE]
pe_com_correct [lemma, in Top.PE]
pe_com_sound [lemma, in Top.PE]
pe_consistent [definition, in Top.PE]
pe_consistent_update [lemma, in Top.PE]
pe_disagree_at [definition, in Top.PE]
pe_disagree_domain [lemma, in Top.PE]
pe_domain [lemma, in Top.PE]
pe_example1 [definition, in Top.PE]
pe_example2 [definition, in Top.PE]
pe_example3 [definition, in Top.PE]
PE_If [constructor, in Top.PE]
PE_IfFalse [constructor, in Top.PE]
PE_IfTrue [constructor, in Top.PE]
pe_lookup [definition, in Top.PE]
pe_peval [inductive, in Top.PE]
pe_peval_intro [constructor, in Top.PE]
pe_program [definition, in Top.PE]
pe_program_correct [lemma, in Top.PE]
pe_remove [definition, in Top.PE]
pe_removes [definition, in Top.PE]
pe_removes_correct [lemma, in Top.PE]
pe_remove_correct [lemma, in Top.PE]
PE_Seq [constructor, in Top.PE]
PE_Skip [constructor, in Top.PE]
pe_state [definition, in Top.PE]
pe_unique [definition, in Top.PE]
pe_unique_correct [lemma, in Top.PE]
pe_update [definition, in Top.PE]
pe_update_consistent [lemma, in Top.PE]
pe_update_correct [lemma, in Top.PE]
pe_update_update_add [lemma, in Top.PE]
pe_update_update_remove [lemma, in Top.PE]
pigeonhole_principle [lemma, in Top.IndProp]
Playground1 [module, in Top.Basics]
Playground1.nat [inductive, in Top.Basics]
Playground1.O [constructor, in Top.Basics]
Playground1.pred [definition, in Top.Basics]
Playground1.S [constructor, in Top.Basics]
Playground2 [module, in Top.Basics]
Playground2.minus [definition, in Top.Basics]
Playground2.mult [definition, in Top.Basics]
Playground2.plus [definition, in Top.Basics]
Playground2.test_mult1 [definition, in Top.Basics]
plus' [definition, in Top.Basics]
plus2 [definition, in Top.Imp]
plus2_spec [lemma, in Top.Imp]
plus3 [definition, in Top.Poly]
plus_assoc [lemma, in Top.Induction]
plus_assoc' [lemma, in Top.Induction]
plus_assoc' [lemma, in Top.IndPrinciples]
plus_assoc'' [lemma, in Top.Induction]
plus_ble_compat_l [lemma, in Top.Induction]
plus_comm [lemma, in Top.Induction]
plus_comm' [lemma, in Top.IndPrinciples]
plus_comm'' [lemma, in Top.IndPrinciples]
plus_comm3 [lemma, in Top.Logic]
plus_comm3_take2 [lemma, in Top.Logic]
plus_comm_ext [lemma, in Top.Logic]
plus_fact [definition, in Top.Logic]
plus_fact_is_true [lemma, in Top.Logic]
plus_id_example [lemma, in Top.Basics]
plus_id_exercise [lemma, in Top.Basics]
plus_lt [lemma, in Top.IndProp]
plus_n_n_injective [lemma, in Top.Tactics]
plus_n_O [lemma, in Top.Basics]
plus_n_O [lemma, in Top.Induction]
plus_n_O_firsttry [lemma, in Top.Induction]
plus_n_O_secondtry [lemma, in Top.Induction]
plus_n_Sm [lemma, in Top.Induction]
plus_one_r' [lemma, in Top.IndPrinciples]
plus_O_n [lemma, in Top.Basics]
plus_O_n' [lemma, in Top.Basics]
plus_rearrange [lemma, in Top.Induction]
plus_rearrange_firsttry [lemma, in Top.Induction]
plus_swap [lemma, in Top.Induction]
plus_swap' [lemma, in Top.Induction]
plus_1_l [lemma, in Top.Basics]
plus_1_neq_0 [lemma, in Top.Basics]
plus_1_neq_0' [lemma, in Top.Basics]
plus_1_neq_0_firsttry [lemma, in Top.Basics]
plus_2_2_is_4 [lemma, in Top.Logic]
Poly [library]
post [definition, in Top.Hoare2]
Postscript [library]
pow2 [definition, in Top.Hoare2]
pow2_le_1 [lemma, in Top.Hoare2]
pow2_plus_1 [lemma, in Top.Hoare2]
pre [definition, in Top.Hoare2]
Preface [library]
preorder [definition, in Top.Rel]
preservation [lemma, in Top.Norm]
preservation [lemma, in Top.RecordSub]
preservation [lemma, in Top.Types]
preservation [lemma, in Top.Sub]
PreservationProgressReferences [module, in Top.UseAuto]
PreservationProgressReferences.nth_eq_last' [lemma, in Top.UseAuto]
PreservationProgressReferences.preservation [lemma, in Top.UseAuto]
PreservationProgressReferences.preservation' [lemma, in Top.UseAuto]
PreservationProgressReferences.preservation_ref [lemma, in Top.UseAuto]
PreservationProgressReferences.progress [lemma, in Top.UseAuto]
PreservationProgressStlc [module, in Top.UseAuto]
PreservationProgressStlc.preservation [lemma, in Top.UseAuto]
PreservationProgressStlc.preservation' [lemma, in Top.UseAuto]
PreservationProgressStlc.progress [lemma, in Top.UseAuto]
PreservationProgressStlc.progress' [lemma, in Top.UseAuto]
preservation' [lemma, in Top.Types]
prod [inductive, in Top.Poly]
prog [definition, in Top.Smallstep]
program [definition, in Top.PE]
progress [lemma, in Top.RecordSub]
progress [lemma, in Top.Sub]
progress [lemma, in Top.Types]
prog_a [definition, in Top.Equiv]
prog_b [definition, in Top.Equiv]
prog_c [definition, in Top.Equiv]
prog_d [definition, in Top.Equiv]
prog_e [definition, in Top.Equiv]
prog_f [definition, in Top.Equiv]
prog_g [definition, in Top.Equiv]
prog_h [definition, in Top.Equiv]
prog_i [definition, in Top.Equiv]
proj1 [lemma, in Top.Logic]
proj2 [lemma, in Top.Logic]
ProofObjects [library]
Props [module, in Top.ProofObjects]
Props.And [module, in Top.ProofObjects]
Props.And.and [inductive, in Top.ProofObjects]
Props.And.conj [constructor, in Top.ProofObjects]
Props.and_comm [lemma, in Top.ProofObjects]
Props.and_comm' [definition, in Top.ProofObjects]
Props.and_comm'_aux [definition, in Top.ProofObjects]
Props.conj_fact [definition, in Top.ProofObjects]
Props.Ex [module, in Top.ProofObjects]
Props.Ex.ex [inductive, in Top.ProofObjects]
Props.Ex.ex_intro [constructor, in Top.ProofObjects]
Props.ex_ev_Sn [definition, in Top.ProofObjects]
Props.False [inductive, in Top.ProofObjects]
Props.I [constructor, in Top.ProofObjects]
Props.Or [module, in Top.ProofObjects]
Props.Or.or [inductive, in Top.ProofObjects]
Props.Or.or_introl [constructor, in Top.ProofObjects]
Props.Or.or_intror [constructor, in Top.ProofObjects]
Props.or_comm [definition, in Top.ProofObjects]
Props.some_nat_is_even [definition, in Top.ProofObjects]
Props.True [inductive, in Top.ProofObjects]
Pumping [module, in Top.IndProp]
Pumping.napp [definition, in Top.IndProp]
Pumping.napp_plus [lemma, in Top.IndProp]
Pumping.pumping [lemma, in Top.IndProp]
Pumping.pumping_constant [definition, in Top.IndProp]
pup_to_n [definition, in Top.ImpCEvalFun]
pup_to_n [definition, in Top.Imp]
pup_to_2_ceval [lemma, in Top.Imp]
P_m0r [definition, in Top.IndPrinciples]
P_m0r' [definition, in Top.IndPrinciples]
Q
quiz6 [definition, in Top.ProofObjects]R
R [definition, in Top.Norm]R [module, in Top.IndProp]
rcd_types_match [lemma, in Top.RecordSub]
real_fact [definition, in Top.Hoare2]
Records [library]
RecordSub [library]
record_tm [inductive, in Top.RecordSub]
record_ty [inductive, in Top.RecordSub]
red [constructor, in Top.IndPrinciples]
reduce_to_zero' [definition, in Top.Hoare2]
reduce_to_zero_correct' [lemma, in Top.Hoare2]
References [library]
reflect [inductive, in Top.IndProp]
ReflectF [constructor, in Top.IndProp]
ReflectT [constructor, in Top.IndProp]
reflect_iff [lemma, in Top.IndProp]
reflexive [definition, in Top.Rel]
refl_aequiv [lemma, in Top.Equiv]
refl_bequiv [lemma, in Top.Equiv]
refl_cequiv [lemma, in Top.Equiv]
reg_exp [inductive, in Top.IndProp]
reg_exp_ex1 [definition, in Top.IndProp]
reg_exp_ex2 [definition, in Top.IndProp]
reg_exp_ex3 [definition, in Top.IndProp]
reg_exp_ex4 [definition, in Top.IndProp]
reg_exp_of_list [definition, in Top.IndProp]
reg_exp_of_list_spec [lemma, in Top.IndProp]
Rel [library]
relation [definition, in Top.Smallstep]
relation [definition, in Top.Rel]
Repeat [module, in Top.Auto]
repeat [definition, in Top.Poly]
RepeatExercise [module, in Top.Hoare]
RepeatExercise.CAsgn [constructor, in Top.Hoare]
RepeatExercise.ceval [inductive, in Top.Hoare]
RepeatExercise.CIf [constructor, in Top.Hoare]
RepeatExercise.com [inductive, in Top.Hoare]
RepeatExercise.CRepeat [constructor, in Top.Hoare]
RepeatExercise.CSeq [constructor, in Top.Hoare]
RepeatExercise.CSkip [constructor, in Top.Hoare]
RepeatExercise.CWhile [constructor, in Top.Hoare]
RepeatExercise.ex1_repeat [definition, in Top.Hoare]
RepeatExercise.ex1_repeat_works [lemma, in Top.Hoare]
RepeatExercise.E_Ass [constructor, in Top.Hoare]
RepeatExercise.E_IfFalse [constructor, in Top.Hoare]
RepeatExercise.E_IfTrue [constructor, in Top.Hoare]
RepeatExercise.E_Seq [constructor, in Top.Hoare]
RepeatExercise.E_Skip [constructor, in Top.Hoare]
RepeatExercise.E_WhileEnd [constructor, in Top.Hoare]
RepeatExercise.E_WhileLoop [constructor, in Top.Hoare]
RepeatExercise.hoare_triple [definition, in Top.Hoare]
RepeatExercise.::x_'/'_x_'\\'_x [notation, in Top.Hoare]
RepeatExercise.::x_'::='_x [notation, in Top.Hoare]
RepeatExercise.::x_';;'_x [notation, in Top.Hoare]
RepeatExercise.::'IFB'_x_'THEN'_x_'ELSE'_x_'FI' [notation, in Top.Hoare]
RepeatExercise.::'REPEAT'_x_'UNTIL'_x_'END' [notation, in Top.Hoare]
RepeatExercise.::'SKIP' [notation, in Top.Hoare]
RepeatExercise.::'WHILE'_x_'DO'_x_'END' [notation, in Top.Hoare]
{{'_x_'}}'_x_'{{'_x_'}}'">RepeatExercise.::'{{'_x_'}}'_x_'{{'_x_'}}' [notation, in Top.Hoare]
repeats [inductive, in Top.IndProp]
repeat' [definition, in Top.Poly]
repeat'' [definition, in Top.Poly]
repeat''' [definition, in Top.Poly]
Repeat.CAsgn [constructor, in Top.Auto]
Repeat.ceval [inductive, in Top.Auto]
Repeat.ceval_deterministic [lemma, in Top.Auto]
Repeat.ceval_deterministic' [lemma, in Top.Auto]
Repeat.CIf [constructor, in Top.Auto]
Repeat.com [inductive, in Top.Auto]
Repeat.CRepeat [constructor, in Top.Auto]
Repeat.CSeq [constructor, in Top.Auto]
Repeat.CSkip [constructor, in Top.Auto]
Repeat.CWhile [constructor, in Top.Auto]
Repeat.E_Ass [constructor, in Top.Auto]
Repeat.E_IfFalse [constructor, in Top.Auto]
Repeat.E_IfTrue [constructor, in Top.Auto]
Repeat.E_RepeatEnd [constructor, in Top.Auto]
Repeat.E_RepeatLoop [constructor, in Top.Auto]
Repeat.E_Seq [constructor, in Top.Auto]
Repeat.E_Skip [constructor, in Top.Auto]
Repeat.E_WhileEnd [constructor, in Top.Auto]
Repeat.E_WhileLoop [constructor, in Top.Auto]
Repeat.::x_'/'_x_'\\'_x [notation, in Top.Auto]
Repeat.::x_'::='_x [notation, in Top.Auto]
Repeat.::x_';'_x [notation, in Top.Auto]
Repeat.::'IFB'_x_'THEN'_x_'ELSE'_x_'FI' [notation, in Top.Auto]
Repeat.::'REPEAT'_x_'UNTIL'_x_'END' [notation, in Top.Auto]
Repeat.::'SKIP' [notation, in Top.Auto]
Repeat.::'WHILE'_x_'DO'_x_'END' [notation, in Top.Auto]
restricted_excluded_middle [lemma, in Top.Logic]
rev [definition, in Top.Poly]
rev_append [definition, in Top.Logic]
rev_app_distr [lemma, in Top.Poly]
rev_exercise1 [lemma, in Top.Tactics]
rev_involutive [lemma, in Top.Poly]
re_chars [definition, in Top.IndProp]
re_not_empty [definition, in Top.IndProp]
re_not_empty_correct [lemma, in Top.IndProp]
rgb [inductive, in Top.IndPrinciples]
RingDemo [module, in Top.UseAuto]
RingDemo.ring_demo [lemma, in Top.UseAuto]
rm [definition, in Top.LibTactics]
rsc_R [lemma, in Top.Rel]
rsc_trans [lemma, in Top.Rel]
RTcons [constructor, in Top.RecordSub]
rtcons [constructor, in Top.RecordSub]
rtc_rsc_coincide [lemma, in Top.Rel]
RTnil [constructor, in Top.RecordSub]
rtnil [constructor, in Top.RecordSub]
rt1n_refl [constructor, in Top.Rel]
rt1n_trans [constructor, in Top.Rel]
rt_refl [constructor, in Top.Rel]
rt_step [constructor, in Top.Rel]
rt_trans [constructor, in Top.Rel]
R.c1 [constructor, in Top.IndProp]
R.c2 [constructor, in Top.IndProp]
R.c3 [constructor, in Top.IndProp]
R.c4 [constructor, in Top.IndProp]
R.c5 [constructor, in Top.IndProp]
R.fR [definition, in Top.IndProp]
R.R [inductive, in Top.IndProp]
R.R_equiv_fR [lemma, in Top.IndProp]
R_halts [lemma, in Top.Norm]
R_typable_empty [lemma, in Top.Norm]
S
sample_proof [definition, in Top.HoareAsLogic]saturday [constructor, in Top.Basics]
search_depth_0 [lemma, in Top.UseAuto]
search_depth_1 [lemma, in Top.UseAuto]
search_depth_3 [lemma, in Top.UseAuto]
search_depth_4 [lemma, in Top.UseAuto]
search_depth_5 [lemma, in Top.UseAuto]
Semantics [module, in Top.UseAuto]
Semantics.multistep_eval_ind [lemma, in Top.UseAuto]
Semantics.multistep__eval [lemma, in Top.UseAuto]
Semantics.multistep__eval' [lemma, in Top.UseAuto]
Semantics.multistep__eval'' [lemma, in Top.UseAuto]
seq_assoc [lemma, in Top.Equiv]
SfLib [library]
sillyfun [definition, in Top.Tactics]
sillyfun1 [definition, in Top.Tactics]
sillyfun1_odd [lemma, in Top.Tactics]
sillyfun1_odd_FAILED [lemma, in Top.Tactics]
sillyfun_false [lemma, in Top.Tactics]
silly1 [lemma, in Top.Tactics]
silly1 [lemma, in Top.Hoare]
silly2 [lemma, in Top.Tactics]
silly2 [lemma, in Top.Hoare]
silly2a [lemma, in Top.Tactics]
silly2_eassumption [lemma, in Top.Hoare]
silly2_fixed [lemma, in Top.Hoare]
silly3 [lemma, in Top.Tactics]
silly3' [lemma, in Top.Tactics]
silly3_firsttry [lemma, in Top.Tactics]
silly_ex [lemma, in Top.Tactics]
silly_fact_1 [lemma, in Top.Tactics]
silly_fact_2 [lemma, in Top.Tactics]
silly_fact_2' [lemma, in Top.Tactics]
silly_fact_2_FAILED [lemma, in Top.Tactics]
SimpleArith1 [module, in Top.Smallstep]
SimpleArith1.step [inductive, in Top.Smallstep]
SimpleArith1.ST_PlusConstConst [constructor, in Top.Smallstep]
SimpleArith1.ST_Plus1 [constructor, in Top.Smallstep]
SimpleArith1.ST_Plus2 [constructor, in Top.Smallstep]
SimpleArith1.test_step_1 [definition, in Top.Smallstep]
SimpleArith1.test_step_2 [definition, in Top.Smallstep]
SimpleArith1.::x_'==>'_x [notation, in Top.Smallstep]
SimpleArith2 [module, in Top.Smallstep]
SimpleArith2.step_deterministic [lemma, in Top.Smallstep]
SimpleArith2.step_deterministic_alt [lemma, in Top.Smallstep]
sinstr [inductive, in Top.Imp]
SkipExample [module, in Top.UseTactics]
SkipExample.astep_example1 [definition, in Top.UseTactics]
SkipExample.ceval_deterministic [lemma, in Top.UseTactics]
SkipExample.demo_skipH [lemma, in Top.UseTactics]
SkipExample.mult_0_plus [lemma, in Top.UseTactics]
skip_axiom [variable, in Top.LibTactics]
skip_left [lemma, in Top.Equiv]
skip_right [lemma, in Top.Equiv]
SLoad [constructor, in Top.Imp]
slow_assignment_dec [definition, in Top.Hoare2]
slow_assignment_dec_correct [lemma, in Top.Hoare2]
Smallstep [library]
SMinus [constructor, in Top.Imp]
SMult [constructor, in Top.Imp]
snd [definition, in Top.Poly]
Sn_le_Sm__n_le_m [lemma, in Top.IndProp]
solved_by_jauto [lemma, in Top.UseAuto]
solving_by_apply [lemma, in Top.UseAuto]
solving_by_eapply [lemma, in Top.UseAuto]
solving_by_reflexivity [lemma, in Top.UseAuto]
solving_conj_goal [lemma, in Top.UseAuto]
solving_conj_hyp [lemma, in Top.UseAuto]
solving_conj_hyp' [lemma, in Top.UseAuto]
solving_conj_hyp_forall [lemma, in Top.UseAuto]
solving_conj_more [lemma, in Top.UseAuto]
solving_disj_goal [lemma, in Top.UseAuto]
solving_disj_hyp [lemma, in Top.UseAuto]
solving_exists_goal [lemma, in Top.UseAuto]
solving_exists_hyp [lemma, in Top.UseAuto]
solving_tauto [lemma, in Top.UseAuto]
Some [constructor, in Top.Poly]
SomeE [constructor, in Top.ImpParser]
some_term_is_stuck [definition, in Top.Types]
SortExamples [module, in Top.UseTactics]
SortExamples.ceval_deterministic [lemma, in Top.UseTactics]
soundness [lemma, in Top.Types]
split [definition, in Top.Poly]
split_combine [lemma, in Top.Tactics]
split_combine_statement [definition, in Top.Tactics]
SPlus [constructor, in Top.Imp]
SPush [constructor, in Top.Imp]
sq [constructor, in Top.IndProp]
sqrt_correct [lemma, in Top.Hoare2]
sqrt_dec [definition, in Top.Hoare2]
square [definition, in Top.Tactics]
square_dec [definition, in Top.Hoare2]
square_dec' [definition, in Top.Hoare2]
square_dec'_correct [lemma, in Top.Hoare2]
square_dec_correct [lemma, in Top.Hoare2]
square_mult [lemma, in Top.Tactics]
square_of [inductive, in Top.IndProp]
square_simpler_dec [definition, in Top.Hoare2]
square_simpler_dec_correct [lemma, in Top.Hoare2]
SSSSev__even [lemma, in Top.IndProp]
SS_Load [constructor, in Top.Smallstep]
SS_Minus [constructor, in Top.Smallstep]
SS_Mult [constructor, in Top.Smallstep]
SS_Plus [constructor, in Top.Smallstep]
SS_Push [constructor, in Top.Smallstep]
stack [definition, in Top.Smallstep]
stack_multistep [definition, in Top.Smallstep]
stack_step [inductive, in Top.Smallstep]
stack_step_deterministic [lemma, in Top.Smallstep]
Star [constructor, in Top.IndProp]
star_app [lemma, in Top.IndProp]
star_app [lemma, in Top.IndProp]
star_app [lemma, in Top.IndProp]
state [definition, in Top.Imp]
step [inductive, in Top.Smallstep]
step [inductive, in Top.Types]
step [inductive, in Top.RecordSub]
step [inductive, in Top.Sub]
step [inductive, in Top.Norm]
step_deterministic [lemma, in Top.Types]
step_deterministic [lemma, in Top.Norm]
step_deterministic [lemma, in Top.Smallstep]
step_normalizing [lemma, in Top.Smallstep]
step_normal_form [abbreviation, in Top.Types]
step_normal_form [definition, in Top.Smallstep]
step_normal_form [abbreviation, in Top.Norm]
step_preserves_halting [lemma, in Top.Norm]
step_preserves_R [lemma, in Top.Norm]
step_preserves_record_tm [lemma, in Top.RecordSub]
step_preserves_R' [lemma, in Top.Norm]
step__eval [lemma, in Top.Smallstep]
STLC [module, in Top.Stlc]
Stlc [library]
STLCArith [module, in Top.StlcProp]
STLCArith.tabs [constructor, in Top.StlcProp]
STLCArith.tapp [constructor, in Top.StlcProp]
STLCArith.TArrow [constructor, in Top.StlcProp]
STLCArith.tif0 [constructor, in Top.StlcProp]
STLCArith.tm [inductive, in Top.StlcProp]
STLCArith.tmult [constructor, in Top.StlcProp]
STLCArith.tnat [constructor, in Top.StlcProp]
STLCArith.TNat [constructor, in Top.StlcProp]
STLCArith.tpred [constructor, in Top.StlcProp]
STLCArith.tsucc [constructor, in Top.StlcProp]
STLCArith.tvar [constructor, in Top.StlcProp]
STLCArith.ty [inductive, in Top.StlcProp]
STLCChecker [module, in Top.Typechecking]
STLCChecker.beq_ty [definition, in Top.Typechecking]
STLCChecker.beq_ty_refl [lemma, in Top.Typechecking]
STLCChecker.beq_ty__eq [lemma, in Top.Typechecking]
STLCChecker.type_check [definition, in Top.Typechecking]
STLCChecker.type_checking_complete [lemma, in Top.Typechecking]
STLCChecker.type_checking_sound [lemma, in Top.Typechecking]
STLCExtended [module, in Top.MoreStlc]
STLCExtendedRecords [module, in Top.Records]
STLCExtendedRecords.a [abbreviation, in Top.Records]
STLCExtendedRecords.A [abbreviation, in Top.Records]
STLCExtendedRecords.afi_abs [constructor, in Top.Records]
STLCExtendedRecords.afi_app1 [constructor, in Top.Records]
STLCExtendedRecords.afi_app2 [constructor, in Top.Records]
STLCExtendedRecords.afi_proj [constructor, in Top.Records]
STLCExtendedRecords.afi_rhead [constructor, in Top.Records]
STLCExtendedRecords.afi_rtail [constructor, in Top.Records]
STLCExtendedRecords.afi_var [constructor, in Top.Records]
STLCExtendedRecords.appears_free_in [inductive, in Top.Records]
STLCExtendedRecords.B [abbreviation, in Top.Records]
STLCExtendedRecords.context [definition, in Top.Records]
STLCExtendedRecords.context_invariance [lemma, in Top.Records]
STLCExtendedRecords.f [abbreviation, in Top.Records]
STLCExtendedRecords.FirstTry [module, in Top.Records]
STLCExtendedRecords.FirstTry.alist [definition, in Top.Records]
STLCExtendedRecords.FirstTry.TArrow [constructor, in Top.Records]
STLCExtendedRecords.FirstTry.TBase [constructor, in Top.Records]
STLCExtendedRecords.FirstTry.TRcd [constructor, in Top.Records]
STLCExtendedRecords.FirstTry.ty [inductive, in Top.Records]
STLCExtendedRecords.free_in_context [lemma, in Top.Records]
STLCExtendedRecords.g [abbreviation, in Top.Records]
STLCExtendedRecords.has_type [inductive, in Top.Records]
STLCExtendedRecords.has_type__wf [lemma, in Top.Records]
STLCExtendedRecords.i1 [abbreviation, in Top.Records]
STLCExtendedRecords.i2 [abbreviation, in Top.Records]
STLCExtendedRecords.k [abbreviation, in Top.Records]
STLCExtendedRecords.l [abbreviation, in Top.Records]
STLCExtendedRecords.lookup_field_in_value [lemma, in Top.Records]
STLCExtendedRecords.multistep [abbreviation, in Top.Records]
STLCExtendedRecords.preservation [lemma, in Top.Records]
STLCExtendedRecords.progress [lemma, in Top.Records]
STLCExtendedRecords.record_tm [inductive, in Top.Records]
STLCExtendedRecords.record_ty [inductive, in Top.Records]
STLCExtendedRecords.rtcons [constructor, in Top.Records]
STLCExtendedRecords.RTcons [constructor, in Top.Records]
STLCExtendedRecords.rtnil [constructor, in Top.Records]
STLCExtendedRecords.RTnil [constructor, in Top.Records]
STLCExtendedRecords.step [inductive, in Top.Records]
STLCExtendedRecords.step_preserves_record_tm [lemma, in Top.Records]
STLCExtendedRecords.ST_AppAbs [constructor, in Top.Records]
STLCExtendedRecords.ST_App1 [constructor, in Top.Records]
STLCExtendedRecords.ST_App2 [constructor, in Top.Records]
STLCExtendedRecords.ST_ProjRcd [constructor, in Top.Records]
STLCExtendedRecords.ST_Proj1 [constructor, in Top.Records]
STLCExtendedRecords.ST_Rcd_Head [constructor, in Top.Records]
STLCExtendedRecords.ST_Rcd_Tail [constructor, in Top.Records]
STLCExtendedRecords.subst [definition, in Top.Records]
STLCExtendedRecords.substitution_preserves_typing [lemma, in Top.Records]
STLCExtendedRecords.tabs [constructor, in Top.Records]
STLCExtendedRecords.tapp [constructor, in Top.Records]
STLCExtendedRecords.TArrow [constructor, in Top.Records]
STLCExtendedRecords.TBase [constructor, in Top.Records]
STLCExtendedRecords.tlookup [definition, in Top.Records]
STLCExtendedRecords.Tlookup [definition, in Top.Records]
STLCExtendedRecords.tm [inductive, in Top.Records]
STLCExtendedRecords.tproj [constructor, in Top.Records]
STLCExtendedRecords.TRCons [constructor, in Top.Records]
STLCExtendedRecords.trcons [constructor, in Top.Records]
STLCExtendedRecords.trnil [constructor, in Top.Records]
STLCExtendedRecords.TRNil [constructor, in Top.Records]
STLCExtendedRecords.tvar [constructor, in Top.Records]
STLCExtendedRecords.ty [inductive, in Top.Records]
STLCExtendedRecords.typing_example_2 [lemma, in Top.Records]
STLCExtendedRecords.typing_nonexample [definition, in Top.Records]
STLCExtendedRecords.typing_nonexample_2 [definition, in Top.Records]
STLCExtendedRecords.T_Abs [constructor, in Top.Records]
STLCExtendedRecords.T_App [constructor, in Top.Records]
STLCExtendedRecords.T_Proj [constructor, in Top.Records]
STLCExtendedRecords.T_RCons [constructor, in Top.Records]
STLCExtendedRecords.T_RNil [constructor, in Top.Records]
STLCExtendedRecords.T_Var [constructor, in Top.Records]
STLCExtendedRecords.value [inductive, in Top.Records]
STLCExtendedRecords.v_abs [constructor, in Top.Records]
STLCExtendedRecords.v_rcons [constructor, in Top.Records]
STLCExtendedRecords.v_rnil [constructor, in Top.Records]
STLCExtendedRecords.weird_type [definition, in Top.Records]
STLCExtendedRecords.well_formed_ty [inductive, in Top.Records]
STLCExtendedRecords.wfTArrow [constructor, in Top.Records]
STLCExtendedRecords.wfTBase [constructor, in Top.Records]
STLCExtendedRecords.wfTRCons [constructor, in Top.Records]
STLCExtendedRecords.wfTRNil [constructor, in Top.Records]
STLCExtendedRecords.wf_rcd_lookup [lemma, in Top.Records]
STLCExtendedRecords.::x_'==>'_x [notation, in Top.Records]
STLCExtendedRecords.::x_'==>*'_x [notation, in Top.Records]
STLCExtendedRecords.::x_'|-'_x_'∈'_x [notation, in Top.Records]
STLCExtendedRecords.::'['_x_':='_x_']'_x [notation, in Top.Records]
STLCExtended.afi_abs [constructor, in Top.MoreStlc]
STLCExtended.afi_app1 [constructor, in Top.MoreStlc]
STLCExtended.afi_app2 [constructor, in Top.MoreStlc]
STLCExtended.afi_case0 [constructor, in Top.MoreStlc]
STLCExtended.afi_case1 [constructor, in Top.MoreStlc]
STLCExtended.afi_case2 [constructor, in Top.MoreStlc]
STLCExtended.afi_cons1 [constructor, in Top.MoreStlc]
STLCExtended.afi_cons2 [constructor, in Top.MoreStlc]
STLCExtended.afi_fst [constructor, in Top.MoreStlc]
STLCExtended.afi_if01 [constructor, in Top.MoreStlc]
STLCExtended.afi_if02 [constructor, in Top.MoreStlc]
STLCExtended.afi_if03 [constructor, in Top.MoreStlc]
STLCExtended.afi_inl [constructor, in Top.MoreStlc]
STLCExtended.afi_inr [constructor, in Top.MoreStlc]
STLCExtended.afi_lcase1 [constructor, in Top.MoreStlc]
STLCExtended.afi_lcase2 [constructor, in Top.MoreStlc]
STLCExtended.afi_lcase3 [constructor, in Top.MoreStlc]
STLCExtended.afi_mult1 [constructor, in Top.MoreStlc]
STLCExtended.afi_mult2 [constructor, in Top.MoreStlc]
STLCExtended.afi_pair1 [constructor, in Top.MoreStlc]
STLCExtended.afi_pair2 [constructor, in Top.MoreStlc]
STLCExtended.afi_pred [constructor, in Top.MoreStlc]
STLCExtended.afi_snd [constructor, in Top.MoreStlc]
STLCExtended.afi_succ [constructor, in Top.MoreStlc]
STLCExtended.afi_var [constructor, in Top.MoreStlc]
STLCExtended.appears_free_in [inductive, in Top.MoreStlc]
STLCExtended.context [definition, in Top.MoreStlc]
STLCExtended.context_invariance [lemma, in Top.MoreStlc]
STLCExtended.Examples [module, in Top.MoreStlc]
STLCExtended.Examples.a [abbreviation, in Top.MoreStlc]
STLCExtended.Examples.eo [abbreviation, in Top.MoreStlc]
STLCExtended.Examples.eq [abbreviation, in Top.MoreStlc]
STLCExtended.Examples.even [abbreviation, in Top.MoreStlc]
STLCExtended.Examples.evenodd [abbreviation, in Top.MoreStlc]
STLCExtended.Examples.f [abbreviation, in Top.MoreStlc]
STLCExtended.Examples.FixTest1 [module, in Top.MoreStlc]
STLCExtended.Examples.FixTest1.fact [definition, in Top.MoreStlc]
STLCExtended.Examples.FixTest2 [module, in Top.MoreStlc]
STLCExtended.Examples.FixTest2.map [definition, in Top.MoreStlc]
STLCExtended.Examples.FixTest3 [module, in Top.MoreStlc]
STLCExtended.Examples.FixTest3.equal [definition, in Top.MoreStlc]
STLCExtended.Examples.FixTest4 [module, in Top.MoreStlc]
STLCExtended.Examples.FixTest4.eotest [definition, in Top.MoreStlc]
STLCExtended.Examples.g [abbreviation, in Top.MoreStlc]
STLCExtended.Examples.i1 [abbreviation, in Top.MoreStlc]
STLCExtended.Examples.i2 [abbreviation, in Top.MoreStlc]
STLCExtended.Examples.k [abbreviation, in Top.MoreStlc]
STLCExtended.Examples.l [abbreviation, in Top.MoreStlc]
STLCExtended.Examples.LetTest [module, in Top.MoreStlc]
STLCExtended.Examples.LetTest.test [definition, in Top.MoreStlc]
STLCExtended.Examples.ListTest [module, in Top.MoreStlc]
STLCExtended.Examples.ListTest.test [definition, in Top.MoreStlc]
STLCExtended.Examples.m [abbreviation, in Top.MoreStlc]
STLCExtended.Examples.n [abbreviation, in Top.MoreStlc]
STLCExtended.Examples.Numtest [module, in Top.MoreStlc]
STLCExtended.Examples.Numtest.test [definition, in Top.MoreStlc]
STLCExtended.Examples.odd [abbreviation, in Top.MoreStlc]
STLCExtended.Examples.processSum [abbreviation, in Top.MoreStlc]
STLCExtended.Examples.Prodtest [module, in Top.MoreStlc]
STLCExtended.Examples.Prodtest.test [definition, in Top.MoreStlc]
STLCExtended.Examples.Sumtest1 [module, in Top.MoreStlc]
STLCExtended.Examples.Sumtest1.test [definition, in Top.MoreStlc]
STLCExtended.Examples.Sumtest2 [module, in Top.MoreStlc]
STLCExtended.Examples.Sumtest2.test [definition, in Top.MoreStlc]
STLCExtended.Examples.x [abbreviation, in Top.MoreStlc]
STLCExtended.Examples.y [abbreviation, in Top.MoreStlc]
STLCExtended.free_in_context [lemma, in Top.MoreStlc]
STLCExtended.has_type [inductive, in Top.MoreStlc]
STLCExtended.multistep [abbreviation, in Top.MoreStlc]
STLCExtended.preservation [lemma, in Top.MoreStlc]
STLCExtended.progress [lemma, in Top.MoreStlc]
STLCExtended.step [inductive, in Top.MoreStlc]
STLCExtended.ST_AppAbs [constructor, in Top.MoreStlc]
STLCExtended.ST_App1 [constructor, in Top.MoreStlc]
STLCExtended.ST_App2 [constructor, in Top.MoreStlc]
STLCExtended.ST_Case [constructor, in Top.MoreStlc]
STLCExtended.ST_CaseInl [constructor, in Top.MoreStlc]
STLCExtended.ST_CaseInr [constructor, in Top.MoreStlc]
STLCExtended.ST_Cons1 [constructor, in Top.MoreStlc]
STLCExtended.ST_Cons2 [constructor, in Top.MoreStlc]
STLCExtended.ST_FstPair [constructor, in Top.MoreStlc]
STLCExtended.ST_Fst1 [constructor, in Top.MoreStlc]
STLCExtended.ST_If0Nonzero [constructor, in Top.MoreStlc]
STLCExtended.ST_If0Zero [constructor, in Top.MoreStlc]
STLCExtended.ST_If01 [constructor, in Top.MoreStlc]
STLCExtended.ST_Inl [constructor, in Top.MoreStlc]
STLCExtended.ST_Inr [constructor, in Top.MoreStlc]
STLCExtended.ST_LcaseCons [constructor, in Top.MoreStlc]
STLCExtended.ST_LcaseNil [constructor, in Top.MoreStlc]
STLCExtended.ST_Lcase1 [constructor, in Top.MoreStlc]
STLCExtended.ST_MultNats [constructor, in Top.MoreStlc]
STLCExtended.ST_Mult1 [constructor, in Top.MoreStlc]
STLCExtended.ST_Mult2 [constructor, in Top.MoreStlc]
STLCExtended.ST_Pair1 [constructor, in Top.MoreStlc]
STLCExtended.ST_Pair2 [constructor, in Top.MoreStlc]
STLCExtended.ST_Pred [constructor, in Top.MoreStlc]
STLCExtended.ST_PredNat [constructor, in Top.MoreStlc]
STLCExtended.ST_SndPair [constructor, in Top.MoreStlc]
STLCExtended.ST_Snd1 [constructor, in Top.MoreStlc]
STLCExtended.ST_SuccNat [constructor, in Top.MoreStlc]
STLCExtended.ST_Succ1 [constructor, in Top.MoreStlc]
STLCExtended.subst [definition, in Top.MoreStlc]
STLCExtended.substitution_preserves_typing [lemma, in Top.MoreStlc]
STLCExtended.tabs [constructor, in Top.MoreStlc]
STLCExtended.tapp [constructor, in Top.MoreStlc]
STLCExtended.TArrow [constructor, in Top.MoreStlc]
STLCExtended.tcase [constructor, in Top.MoreStlc]
STLCExtended.tcons [constructor, in Top.MoreStlc]
STLCExtended.tfix [constructor, in Top.MoreStlc]
STLCExtended.tfst [constructor, in Top.MoreStlc]
STLCExtended.tif0 [constructor, in Top.MoreStlc]
STLCExtended.tinl [constructor, in Top.MoreStlc]
STLCExtended.tinr [constructor, in Top.MoreStlc]
STLCExtended.tlcase [constructor, in Top.MoreStlc]
STLCExtended.tlet [constructor, in Top.MoreStlc]
STLCExtended.TList [constructor, in Top.MoreStlc]
STLCExtended.tm [inductive, in Top.MoreStlc]
STLCExtended.tmult [constructor, in Top.MoreStlc]
STLCExtended.tnat [constructor, in Top.MoreStlc]
STLCExtended.TNat [constructor, in Top.MoreStlc]
STLCExtended.tnil [constructor, in Top.MoreStlc]
STLCExtended.tpair [constructor, in Top.MoreStlc]
STLCExtended.tpred [constructor, in Top.MoreStlc]
STLCExtended.TProd [constructor, in Top.MoreStlc]
STLCExtended.tsnd [constructor, in Top.MoreStlc]
STLCExtended.tsucc [constructor, in Top.MoreStlc]
STLCExtended.TSum [constructor, in Top.MoreStlc]
STLCExtended.TUnit [constructor, in Top.MoreStlc]
STLCExtended.tunit [constructor, in Top.MoreStlc]
STLCExtended.tvar [constructor, in Top.MoreStlc]
STLCExtended.ty [inductive, in Top.MoreStlc]
STLCExtended.T_Abs [constructor, in Top.MoreStlc]
STLCExtended.T_App [constructor, in Top.MoreStlc]
STLCExtended.T_Case [constructor, in Top.MoreStlc]
STLCExtended.T_Cons [constructor, in Top.MoreStlc]
STLCExtended.T_Fst [constructor, in Top.MoreStlc]
STLCExtended.T_If0 [constructor, in Top.MoreStlc]
STLCExtended.T_Inl [constructor, in Top.MoreStlc]
STLCExtended.T_Inr [constructor, in Top.MoreStlc]
STLCExtended.T_Lcase [constructor, in Top.MoreStlc]
STLCExtended.T_Mult [constructor, in Top.MoreStlc]
STLCExtended.T_Nat [constructor, in Top.MoreStlc]
STLCExtended.T_Nil [constructor, in Top.MoreStlc]
STLCExtended.T_Pair [constructor, in Top.MoreStlc]
STLCExtended.T_Pred [constructor, in Top.MoreStlc]
STLCExtended.T_Snd [constructor, in Top.MoreStlc]
STLCExtended.T_Succ [constructor, in Top.MoreStlc]
STLCExtended.T_Unit [constructor, in Top.MoreStlc]
STLCExtended.T_Var [constructor, in Top.MoreStlc]
STLCExtended.value [inductive, in Top.MoreStlc]
STLCExtended.v_abs [constructor, in Top.MoreStlc]
STLCExtended.v_inl [constructor, in Top.MoreStlc]
STLCExtended.v_inr [constructor, in Top.MoreStlc]
STLCExtended.v_lcons [constructor, in Top.MoreStlc]
STLCExtended.v_lnil [constructor, in Top.MoreStlc]
STLCExtended.v_nat [constructor, in Top.MoreStlc]
STLCExtended.v_pair [constructor, in Top.MoreStlc]
STLCExtended.v_unit [constructor, in Top.MoreStlc]
STLCExtended.::x_'==>'_x [notation, in Top.MoreStlc]
STLCExtended.::x_'==>*'_x [notation, in Top.MoreStlc]
STLCExtended.::x_'|-'_x_'∈'_x [notation, in Top.MoreStlc]
STLCExtended.::'['_x_':='_x_']'_x [notation, in Top.MoreStlc]
STLCProp [module, in Top.StlcProp]
StlcProp [library]
STLCProp.afi_abs [constructor, in Top.StlcProp]
STLCProp.afi_app1 [constructor, in Top.StlcProp]
STLCProp.afi_app2 [constructor, in Top.StlcProp]
STLCProp.afi_if1 [constructor, in Top.StlcProp]
STLCProp.afi_if2 [constructor, in Top.StlcProp]
STLCProp.afi_if3 [constructor, in Top.StlcProp]
STLCProp.afi_var [constructor, in Top.StlcProp]
STLCProp.appears_free_in [inductive, in Top.StlcProp]
STLCProp.canonical_forms_bool [lemma, in Top.StlcProp]
STLCProp.canonical_forms_fun [lemma, in Top.StlcProp]
STLCProp.closed [definition, in Top.StlcProp]
STLCProp.context_invariance [lemma, in Top.StlcProp]
STLCProp.free_in_context [lemma, in Top.StlcProp]
STLCProp.preservation [lemma, in Top.StlcProp]
STLCProp.progress [lemma, in Top.StlcProp]
STLCProp.progress' [lemma, in Top.StlcProp]
STLCProp.soundness [lemma, in Top.StlcProp]
STLCProp.stuck [definition, in Top.StlcProp]
STLCProp.substitution_preserves_typing [lemma, in Top.StlcProp]
STLCProp.typable_empty__closed [lemma, in Top.StlcProp]
STLCRef [module, in Top.References]
STLCRef.afi_abs [constructor, in Top.References]
STLCRef.afi_app1 [constructor, in Top.References]
STLCRef.afi_app2 [constructor, in Top.References]
STLCRef.afi_assign1 [constructor, in Top.References]
STLCRef.afi_assign2 [constructor, in Top.References]
STLCRef.afi_deref [constructor, in Top.References]
STLCRef.afi_if0_1 [constructor, in Top.References]
STLCRef.afi_if0_2 [constructor, in Top.References]
STLCRef.afi_if0_3 [constructor, in Top.References]
STLCRef.afi_mult1 [constructor, in Top.References]
STLCRef.afi_mult2 [constructor, in Top.References]
STLCRef.afi_pred [constructor, in Top.References]
STLCRef.afi_ref [constructor, in Top.References]
STLCRef.afi_succ [constructor, in Top.References]
STLCRef.afi_var [constructor, in Top.References]
STLCRef.appears_free_in [inductive, in Top.References]
STLCRef.assign_pres_store_typing [lemma, in Top.References]
STLCRef.context [definition, in Top.References]
STLCRef.context_invariance [lemma, in Top.References]
STLCRef.ExampleVariables [module, in Top.References]
STLCRef.ExampleVariables.r [definition, in Top.References]
STLCRef.ExampleVariables.s [definition, in Top.References]
STLCRef.ExampleVariables.x [definition, in Top.References]
STLCRef.ExampleVariables.y [definition, in Top.References]
STLCRef.extends [inductive, in Top.References]
STLCRef.extends_app [lemma, in Top.References]
STLCRef.extends_cons [constructor, in Top.References]
STLCRef.extends_lookup [lemma, in Top.References]
STLCRef.extends_nil [constructor, in Top.References]
STLCRef.extends_refl [lemma, in Top.References]
STLCRef.free_in_context [lemma, in Top.References]
STLCRef.has_type [inductive, in Top.References]
STLCRef.length_extends [lemma, in Top.References]
STLCRef.length_replace [lemma, in Top.References]
STLCRef.lookup_replace_eq [lemma, in Top.References]
STLCRef.lookup_replace_neq [lemma, in Top.References]
STLCRef.multistep [definition, in Top.References]
STLCRef.nth_eq_last [lemma, in Top.References]
STLCRef.preservation [lemma, in Top.References]
STLCRef.preservation_theorem [definition, in Top.References]
STLCRef.preservation_wrong1 [lemma, in Top.References]
STLCRef.preservation_wrong2 [lemma, in Top.References]
STLCRef.progress [lemma, in Top.References]
STLCRef.RefsAndNontermination [module, in Top.References]
STLCRef.RefsAndNontermination.factorial [definition, in Top.References]
STLCRef.RefsAndNontermination.factorial_type [lemma, in Top.References]
STLCRef.RefsAndNontermination.loop [definition, in Top.References]
STLCRef.RefsAndNontermination.loop_fun [definition, in Top.References]
STLCRef.RefsAndNontermination.loop_fun_step_self [lemma, in Top.References]
STLCRef.RefsAndNontermination.loop_steps_to_loop_fun [lemma, in Top.References]
STLCRef.RefsAndNontermination.loop_typeable [lemma, in Top.References]
STLCRef.RefsAndNontermination.multistep1 [definition, in Top.References]
STLCRef.RefsAndNontermination.sc_one [constructor, in Top.References]
STLCRef.RefsAndNontermination.sc_step [constructor, in Top.References]
STLCRef.RefsAndNontermination.step_closure [inductive, in Top.References]
STLCRef.RefsAndNontermination.::x_'/'_x_'==>+'_x_'/'_x [notation, in Top.References]
STLCRef.replace [definition, in Top.References]
STLCRef.replace_nil [lemma, in Top.References]
STLCRef.step [inductive, in Top.References]
STLCRef.store [definition, in Top.References]
STLCRef.store_lookup [definition, in Top.References]
STLCRef.store_Tlookup [definition, in Top.References]
STLCRef.store_ty [definition, in Top.References]
STLCRef.store_weakening [lemma, in Top.References]
STLCRef.store_well_typed [definition, in Top.References]
STLCRef.store_well_typed_app [lemma, in Top.References]
STLCRef.ST_AppAbs [constructor, in Top.References]
STLCRef.ST_App1 [constructor, in Top.References]
STLCRef.ST_App2 [constructor, in Top.References]
STLCRef.ST_Assign [constructor, in Top.References]
STLCRef.ST_Assign1 [constructor, in Top.References]
STLCRef.ST_Assign2 [constructor, in Top.References]
STLCRef.ST_Deref [constructor, in Top.References]
STLCRef.ST_DerefLoc [constructor, in Top.References]
STLCRef.ST_If0 [constructor, in Top.References]
STLCRef.ST_If0_Nonzero [constructor, in Top.References]
STLCRef.ST_If0_Zero [constructor, in Top.References]
STLCRef.ST_MultNats [constructor, in Top.References]
STLCRef.ST_Mult1 [constructor, in Top.References]
STLCRef.ST_Mult2 [constructor, in Top.References]
STLCRef.ST_Pred [constructor, in Top.References]
STLCRef.ST_PredNat [constructor, in Top.References]
STLCRef.ST_Ref [constructor, in Top.References]
STLCRef.ST_RefValue [constructor, in Top.References]
STLCRef.ST_Succ [constructor, in Top.References]
STLCRef.ST_SuccNat [constructor, in Top.References]
STLCRef.subst [definition, in Top.References]
STLCRef.substitution_preserves_typing [lemma, in Top.References]
STLCRef.tabs [constructor, in Top.References]
STLCRef.tapp [constructor, in Top.References]
STLCRef.TArrow [constructor, in Top.References]
STLCRef.tassign [constructor, in Top.References]
STLCRef.tderef [constructor, in Top.References]
STLCRef.tif0 [constructor, in Top.References]
STLCRef.tloc [constructor, in Top.References]
STLCRef.tm [inductive, in Top.References]
STLCRef.tmult [constructor, in Top.References]
STLCRef.TNat [constructor, in Top.References]
STLCRef.tnat [constructor, in Top.References]
STLCRef.tpred [constructor, in Top.References]
STLCRef.tref [constructor, in Top.References]
STLCRef.TRef [constructor, in Top.References]
STLCRef.tseq [definition, in Top.References]
STLCRef.tsucc [constructor, in Top.References]
STLCRef.tunit [constructor, in Top.References]
STLCRef.TUnit [constructor, in Top.References]
STLCRef.tvar [constructor, in Top.References]
STLCRef.ty [inductive, in Top.References]
STLCRef.T_Abs [constructor, in Top.References]
STLCRef.T_App [constructor, in Top.References]
STLCRef.T_Assign [constructor, in Top.References]
STLCRef.T_Deref [constructor, in Top.References]
STLCRef.T_If0 [constructor, in Top.References]
STLCRef.T_Loc [constructor, in Top.References]
STLCRef.T_Mult [constructor, in Top.References]
STLCRef.T_Nat [constructor, in Top.References]
STLCRef.T_Pred [constructor, in Top.References]
STLCRef.T_Ref [constructor, in Top.References]
STLCRef.T_Succ [constructor, in Top.References]
STLCRef.T_Unit [constructor, in Top.References]
STLCRef.T_Var [constructor, in Top.References]
STLCRef.value [inductive, in Top.References]
STLCRef.v_abs [constructor, in Top.References]
STLCRef.v_loc [constructor, in Top.References]
STLCRef.v_nat [constructor, in Top.References]
STLCRef.v_unit [constructor, in Top.References]
STLCRef.::x_'/'_x_'==>'_x_'/'_x [notation, in Top.References]
STLCRef.::x_'/'_x_'==>*'_x_'/'_x [notation, in Top.References]
STLCRef.::x_';'_x_'|-'_x_'∈'_x [notation, in Top.References]
STLCRef.::'['_x_':='_x_']'_x [notation, in Top.References]
STLC.context [definition, in Top.Stlc]
STLC.has_type [inductive, in Top.Stlc]
STLC.idB [abbreviation, in Top.Stlc]
STLC.idBB [abbreviation, in Top.Stlc]
STLC.idBBBB [abbreviation, in Top.Stlc]
STLC.k [abbreviation, in Top.Stlc]
STLC.multistep [abbreviation, in Top.Stlc]
STLC.notB [abbreviation, in Top.Stlc]
STLC.step [inductive, in Top.Stlc]
STLC.step_example1 [lemma, in Top.Stlc]
STLC.step_example1' [lemma, in Top.Stlc]
STLC.step_example2 [lemma, in Top.Stlc]
STLC.step_example2' [lemma, in Top.Stlc]
STLC.step_example3 [lemma, in Top.Stlc]
STLC.step_example3' [lemma, in Top.Stlc]
STLC.step_example4 [lemma, in Top.Stlc]
STLC.step_example4' [lemma, in Top.Stlc]
STLC.step_example5 [lemma, in Top.Stlc]
STLC.step_example5_with_normalize [lemma, in Top.Stlc]
STLC.ST_AppAbs [constructor, in Top.Stlc]
STLC.ST_App1 [constructor, in Top.Stlc]
STLC.ST_App2 [constructor, in Top.Stlc]
STLC.ST_If [constructor, in Top.Stlc]
STLC.ST_IfFalse [constructor, in Top.Stlc]
STLC.ST_IfTrue [constructor, in Top.Stlc]
STLC.subst [definition, in Top.Stlc]
STLC.substi [inductive, in Top.Stlc]
STLC.substi_correct [lemma, in Top.Stlc]
STLC.s_var1 [constructor, in Top.Stlc]
STLC.tabs [constructor, in Top.Stlc]
STLC.tapp [constructor, in Top.Stlc]
STLC.TArrow [constructor, in Top.Stlc]
STLC.TBool [constructor, in Top.Stlc]
STLC.tfalse [constructor, in Top.Stlc]
STLC.tif [constructor, in Top.Stlc]
STLC.tm [inductive, in Top.Stlc]
STLC.ttrue [constructor, in Top.Stlc]
STLC.tvar [constructor, in Top.Stlc]
STLC.ty [inductive, in Top.Stlc]
STLC.typing_example_1 [definition, in Top.Stlc]
STLC.typing_example_1' [definition, in Top.Stlc]
STLC.typing_example_2 [definition, in Top.Stlc]
STLC.typing_example_2_full [definition, in Top.Stlc]
STLC.typing_example_3 [definition, in Top.Stlc]
STLC.typing_nonexample_1 [definition, in Top.Stlc]
STLC.typing_nonexample_3 [definition, in Top.Stlc]
STLC.T_Abs [constructor, in Top.Stlc]
STLC.T_App [constructor, in Top.Stlc]
STLC.T_False [constructor, in Top.Stlc]
STLC.T_If [constructor, in Top.Stlc]
STLC.T_True [constructor, in Top.Stlc]
STLC.T_Var [constructor, in Top.Stlc]
STLC.value [inductive, in Top.Stlc]
STLC.v_abs [constructor, in Top.Stlc]
STLC.v_false [constructor, in Top.Stlc]
STLC.v_true [constructor, in Top.Stlc]
STLC.x [definition, in Top.Stlc]
STLC.y [definition, in Top.Stlc]
STLC.z [definition, in Top.Stlc]
STLC.::x_'==>'_x [notation, in Top.Stlc]
STLC.::x_'==>*'_x [notation, in Top.Stlc]
STLC.::x_'|-'_x_'∈'_x [notation, in Top.Stlc]
STLC.::'['_x_':='_x_']'_x [notation, in Top.Stlc]
string_of_list [definition, in Top.ImpParser]
strong_progress [lemma, in Top.Smallstep]
stuck [definition, in Top.Types]
st12 [definition, in Top.Auto]
st21 [definition, in Top.Auto]
ST_AppAbs [constructor, in Top.RecordSub]
ST_AppAbs [constructor, in Top.Sub]
ST_AppAbs [constructor, in Top.Norm]
ST_App1 [constructor, in Top.RecordSub]
ST_App1 [constructor, in Top.Sub]
ST_App1 [constructor, in Top.Norm]
ST_App2 [constructor, in Top.RecordSub]
ST_App2 [constructor, in Top.Norm]
ST_App2 [constructor, in Top.Sub]
ST_Fst [constructor, in Top.Norm]
ST_FstPair [constructor, in Top.Norm]
ST_If [constructor, in Top.Norm]
ST_If [constructor, in Top.Types]
ST_If [constructor, in Top.Sub]
ST_IfFalse [constructor, in Top.Types]
ST_IfFalse [constructor, in Top.Sub]
ST_IfFalse [constructor, in Top.Norm]
ST_IfTrue [constructor, in Top.Sub]
ST_IfTrue [constructor, in Top.Norm]
ST_IfTrue [constructor, in Top.Types]
ST_Iszero [constructor, in Top.Types]
ST_IszeroSucc [constructor, in Top.Types]
ST_IszeroZero [constructor, in Top.Types]
ST_Pair1 [constructor, in Top.Norm]
ST_Pair2 [constructor, in Top.Norm]
ST_PlusConstConst [constructor, in Top.Smallstep]
ST_Plus1 [constructor, in Top.Smallstep]
ST_Plus2 [constructor, in Top.Smallstep]
ST_Pred [constructor, in Top.Types]
ST_PredSucc [constructor, in Top.Types]
ST_PredZero [constructor, in Top.Types]
ST_ProjRcd [constructor, in Top.RecordSub]
ST_Proj1 [constructor, in Top.RecordSub]
ST_Rcd_Head [constructor, in Top.RecordSub]
ST_Rcd_Tail [constructor, in Top.RecordSub]
ST_Snd [constructor, in Top.Norm]
ST_SndPair [constructor, in Top.Norm]
ST_Succ [constructor, in Top.Types]
Sub [library]
subst [definition, in Top.Sub]
subst [definition, in Top.Norm]
subst [definition, in Top.RecordSub]
substitution_preserves_typing [lemma, in Top.RecordSub]
substitution_preserves_typing [lemma, in Top.Sub]
substitution_preserves_typing [lemma, in Top.Norm]
subst_aexp [definition, in Top.Equiv]
subst_aexp_ex [definition, in Top.Equiv]
subst_closed [lemma, in Top.Norm]
subst_equiv_property [definition, in Top.Equiv]
subst_inequiv [lemma, in Top.Equiv]
subst_msubst [lemma, in Top.Norm]
subst_not_afi [lemma, in Top.Norm]
subtract_slowly [definition, in Top.Imp]
subtract_slowly_body [definition, in Top.Imp]
subtract_slowly_dec [definition, in Top.Hoare2]
subtract_slowly_dec_correct [lemma, in Top.Hoare2]
subtract_3_from_5_slowly [definition, in Top.Imp]
subtype [axiom, in Top.UseAuto]
subtype [inductive, in Top.Sub]
subtype [inductive, in Top.RecordSub]
subtype_refl [axiom, in Top.UseAuto]
subtype_trans [axiom, in Top.UseAuto]
subtype__wf [lemma, in Top.RecordSub]
SubtypingInversion [module, in Top.UseAuto]
SubtypingInversion.abs_arrow [lemma, in Top.UseAuto]
SubtypingInversion.abs_arrow' [lemma, in Top.UseAuto]
SubtypingInversion.substitution_preserves_typing [lemma, in Top.UseAuto]
sub_inversion_arrow [lemma, in Top.RecordSub]
sub_inversion_arrow [lemma, in Top.Sub]
sub_inversion_Bool [lemma, in Top.Sub]
succ_hastype_nat__hastype_nat [definition, in Top.Types]
succ_inj [lemma, in Top.Logic]
sunday [constructor, in Top.Basics]
swap [definition, in Top.Hoare2]
swap_correct [lemma, in Top.Hoare2]
swap_dec [definition, in Top.Hoare2]
swap_exercise [lemma, in Top.Hoare]
swap_if_branches [lemma, in Top.Equiv]
swap_noninterfering_assignments [lemma, in Top.Equiv]
swap_program [definition, in Top.Hoare]
swap_subst [lemma, in Top.Norm]
Symbols [library]
symmetric [definition, in Top.Rel]
sym_aequiv [lemma, in Top.Equiv]
sym_bequiv [lemma, in Top.Equiv]
sym_cequiv [lemma, in Top.Equiv]
S_Arrow [constructor, in Top.RecordSub]
S_Arrow [constructor, in Top.Sub]
s_compile [definition, in Top.Imp]
s_compile1 [definition, in Top.Imp]
s_compile_correct [lemma, in Top.Imp]
s_execute [definition, in Top.Imp]
s_execute1 [definition, in Top.Imp]
s_execute2 [definition, in Top.Imp]
S_inj [lemma, in Top.Tactics]
S_injective [lemma, in Top.Tactics]
S_nbeq_0 [lemma, in Top.Induction]
S_RcdDepth [constructor, in Top.RecordSub]
S_RcdPerm [constructor, in Top.RecordSub]
S_RcdWidth [constructor, in Top.RecordSub]
S_Refl [constructor, in Top.Sub]
S_Refl [constructor, in Top.RecordSub]
S_Top [constructor, in Top.RecordSub]
S_Top [constructor, in Top.Sub]
S_Trans [constructor, in Top.Sub]
S_Trans [constructor, in Top.RecordSub]
T
tabs [constructor, in Top.Sub]tabs [constructor, in Top.RecordSub]
tabs [constructor, in Top.Norm]
Tactics [library]
tapp [constructor, in Top.Norm]
tapp [constructor, in Top.Sub]
tapp [constructor, in Top.RecordSub]
TArrow [constructor, in Top.RecordSub]
TArrow [constructor, in Top.Norm]
TArrow [constructor, in Top.Sub]
tass [definition, in Top.Norm]
TBase [constructor, in Top.RecordSub]
TBase [constructor, in Top.Sub]
TBool [constructor, in Top.Sub]
TBool [constructor, in Top.Norm]
TBool [constructor, in Top.Types]
Temp1 [module, in Top.Smallstep]
Temp1.step [inductive, in Top.Smallstep]
Temp1.ST_PlusConstConst [constructor, in Top.Smallstep]
Temp1.ST_Plus1 [constructor, in Top.Smallstep]
Temp1.ST_Plus2 [constructor, in Top.Smallstep]
Temp1.value [inductive, in Top.Smallstep]
Temp1.value_not_same_as_normal_form [lemma, in Top.Smallstep]
Temp1.v_const [constructor, in Top.Smallstep]
Temp1.v_funny [constructor, in Top.Smallstep]
Temp1.::x_'==>'_x [notation, in Top.Smallstep]
Temp2 [module, in Top.Smallstep]
Temp2.step [inductive, in Top.Smallstep]
Temp2.ST_Funny [constructor, in Top.Smallstep]
Temp2.ST_PlusConstConst [constructor, in Top.Smallstep]
Temp2.ST_Plus1 [constructor, in Top.Smallstep]
Temp2.ST_Plus2 [constructor, in Top.Smallstep]
Temp2.value [inductive, in Top.Smallstep]
Temp2.value_not_same_as_normal_form [lemma, in Top.Smallstep]
Temp2.v_const [constructor, in Top.Smallstep]
Temp2.::x_'==>'_x [notation, in Top.Smallstep]
Temp3 [module, in Top.Smallstep]
Temp3.step [inductive, in Top.Smallstep]
Temp3.ST_PlusConstConst [constructor, in Top.Smallstep]
Temp3.ST_Plus1 [constructor, in Top.Smallstep]
Temp3.value [inductive, in Top.Smallstep]
Temp3.value_not_same_as_normal_form [lemma, in Top.Smallstep]
Temp3.v_const [constructor, in Top.Smallstep]
Temp3.::x_'==>'_x [notation, in Top.Smallstep]
Temp4 [module, in Top.Smallstep]
Temp4.bool_step_prop1 [definition, in Top.Smallstep]
Temp4.bool_step_prop2 [definition, in Top.Smallstep]
Temp4.bool_step_prop3 [definition, in Top.Smallstep]
Temp4.step [inductive, in Top.Smallstep]
Temp4.step_deterministic [lemma, in Top.Smallstep]
Temp4.strong_progress [lemma, in Top.Smallstep]
Temp4.ST_If [constructor, in Top.Smallstep]
Temp4.ST_IfFalse [constructor, in Top.Smallstep]
Temp4.ST_IfTrue [constructor, in Top.Smallstep]
Temp4.Temp5 [module, in Top.Smallstep]
Temp4.Temp5.bool_step_prop4 [definition, in Top.Smallstep]
Temp4.Temp5.bool_step_prop4_holds [definition, in Top.Smallstep]
Temp4.Temp5.step [inductive, in Top.Smallstep]
Temp4.Temp5.ST_If [constructor, in Top.Smallstep]
Temp4.Temp5.ST_IfFalse [constructor, in Top.Smallstep]
Temp4.Temp5.ST_IfTrue [constructor, in Top.Smallstep]
Temp4.Temp5.::x_'==>'_x [notation, in Top.Smallstep]
Temp4.tfalse [constructor, in Top.Smallstep]
Temp4.tif [constructor, in Top.Smallstep]
Temp4.tm [inductive, in Top.Smallstep]
Temp4.ttrue [constructor, in Top.Smallstep]
Temp4.value [inductive, in Top.Smallstep]
Temp4.v_false [constructor, in Top.Smallstep]
Temp4.v_true [constructor, in Top.Smallstep]
Temp4.::x_'==>'_x [notation, in Top.Smallstep]
testParsing [definition, in Top.ImpParser]
test_andb31 [definition, in Top.Basics]
test_andb32 [definition, in Top.Basics]
test_andb33 [definition, in Top.Basics]
test_andb34 [definition, in Top.Basics]
test_anon_fun' [definition, in Top.Poly]
test_blt_nat1 [definition, in Top.Basics]
test_blt_nat2 [definition, in Top.Basics]
test_blt_nat3 [definition, in Top.Basics]
test_ceval [definition, in Top.ImpCEvalFun]
test_countoddmembers'1 [definition, in Top.Poly]
test_countoddmembers'2 [definition, in Top.Poly]
test_countoddmembers'3 [definition, in Top.Poly]
test_doit3times [definition, in Top.Poly]
test_doit3times' [definition, in Top.Poly]
test_factorial1 [definition, in Top.Basics]
test_factorial2 [definition, in Top.Basics]
test_filter1 [definition, in Top.Poly]
test_filter2 [definition, in Top.Poly]
test_filter2' [definition, in Top.Poly]
test_filter_even_gt7_1 [definition, in Top.Poly]
test_filter_even_gt7_2 [definition, in Top.Poly]
test_flat_map1 [definition, in Top.Poly]
test_hd_error1 [definition, in Top.Poly]
test_hd_error2 [definition, in Top.Poly]
test_leb1 [definition, in Top.Basics]
test_leb2 [definition, in Top.Basics]
test_leb3 [definition, in Top.Basics]
test_length1 [definition, in Top.Poly]
test_map1 [definition, in Top.Poly]
test_map2 [definition, in Top.Poly]
test_map3 [definition, in Top.Poly]
test_multistep_1 [lemma, in Top.Smallstep]
test_multistep_1' [lemma, in Top.Smallstep]
test_multistep_2 [lemma, in Top.Smallstep]
test_multistep_3 [lemma, in Top.Smallstep]
test_multistep_4 [lemma, in Top.Smallstep]
test_nandb1 [definition, in Top.Basics]
test_nandb2 [definition, in Top.Basics]
test_nandb3 [definition, in Top.Basics]
test_nandb4 [definition, in Top.Basics]
test_next_weekday [definition, in Top.Basics]
test_nostutter_1 [definition, in Top.IndProp]
test_nostutter_2 [definition, in Top.IndProp]
test_nostutter_3 [definition, in Top.IndProp]
test_nostutter_4 [definition, in Top.IndProp]
test_nth_error1 [definition, in Top.Poly]
test_nth_error2 [definition, in Top.Poly]
test_nth_error3 [definition, in Top.Poly]
test_oddb1 [definition, in Top.Basics]
test_oddb2 [definition, in Top.Basics]
test_orb1 [definition, in Top.Basics]
test_orb2 [definition, in Top.Basics]
test_orb3 [definition, in Top.Basics]
test_orb4 [definition, in Top.Basics]
test_orb5 [definition, in Top.Basics]
test_partition1 [definition, in Top.Poly]
test_partition2 [definition, in Top.Poly]
test_pe_aexp1 [definition, in Top.PE]
test_pe_bexp1 [definition, in Top.PE]
test_pe_bexp2 [definition, in Top.PE]
test_pe_update [definition, in Top.PE]
test_plus3 [definition, in Top.Poly]
test_plus3' [definition, in Top.Poly]
test_plus3'' [definition, in Top.Poly]
test_repeat1 [definition, in Top.Poly]
test_repeat2 [definition, in Top.Poly]
test_rev1 [definition, in Top.Poly]
test_rev2 [definition, in Top.Poly]
test_split [definition, in Top.Poly]
text_pe_aexp2 [definition, in Top.PE]
tfalse [constructor, in Top.Norm]
tfalse [constructor, in Top.Types]
tfalse [constructor, in Top.Sub]
tfst [constructor, in Top.Norm]
thursday [constructor, in Top.Basics]
tif [constructor, in Top.Types]
tif [constructor, in Top.Norm]
tif [constructor, in Top.Sub]
tiszero [constructor, in Top.Types]
tlookup [definition, in Top.RecordSub]
Tlookup [definition, in Top.RecordSub]
tm [inductive, in Top.RecordSub]
tm [inductive, in Top.Types]
tm [inductive, in Top.Smallstep]
tm [inductive, in Top.Sub]
tm [inductive, in Top.Norm]
TNat [constructor, in Top.Types]
token [definition, in Top.ImpParser]
tokenize [definition, in Top.ImpParser]
tokenize_ex1 [definition, in Top.ImpParser]
tokenize_helper [definition, in Top.ImpParser]
total_map [definition, in Top.Maps]
tpair [constructor, in Top.Norm]
tpred [constructor, in Top.Types]
TProd [constructor, in Top.Norm]
tproj [constructor, in Top.RecordSub]
transitive [definition, in Top.Rel]
transitivity_bad_hint_1 [lemma, in Top.UseAuto]
transitivity_workaround_1 [lemma, in Top.UseAuto]
transitivity_workaround_2 [lemma, in Top.UseAuto]
trans_aequiv [lemma, in Top.Equiv]
trans_bequiv [lemma, in Top.Equiv]
trans_cequiv [lemma, in Top.Equiv]
trans_eq [lemma, in Top.Tactics]
trans_eq_example [definition, in Top.Tactics]
trans_eq_example' [definition, in Top.Tactics]
trans_eq_exercise [definition, in Top.Tactics]
TRCons [constructor, in Top.RecordSub]
trcons [constructor, in Top.RecordSub]
tree [inductive, in Top.IndPrinciples]
trnil [constructor, in Top.RecordSub]
TRNil [constructor, in Top.RecordSub]
true [constructor, in Top.Basics]
True_is_true [lemma, in Top.Logic]
tr_rev [definition, in Top.Logic]
tr_rev_correct [lemma, in Top.Logic]
tsnd [constructor, in Top.Norm]
tsucc [constructor, in Top.Types]
TTop [constructor, in Top.RecordSub]
TTop [constructor, in Top.Sub]
ttrue [constructor, in Top.Sub]
ttrue [constructor, in Top.Norm]
ttrue [constructor, in Top.Types]
tuesday [constructor, in Top.Basics]
tunit [constructor, in Top.Sub]
TUnit [constructor, in Top.Sub]
tvar [constructor, in Top.Sub]
tvar [constructor, in Top.Norm]
tvar [constructor, in Top.RecordSub]
two_loops_correct [lemma, in Top.Hoare2]
two_loops_dec [definition, in Top.Hoare2]
ty [inductive, in Top.RecordSub]
ty [inductive, in Top.Sub]
ty [inductive, in Top.Types]
ty [inductive, in Top.Norm]
typ [axiom, in Top.UseAuto]
typable_empty__closed [lemma, in Top.Norm]
Typechecking [library]
Types [library]
typing_inversion_abs [lemma, in Top.RecordSub]
typing_inversion_abs [lemma, in Top.Sub]
typing_inversion_app [lemma, in Top.RecordSub]
typing_inversion_app [lemma, in Top.Sub]
typing_inversion_false [lemma, in Top.Sub]
typing_inversion_if [lemma, in Top.Sub]
typing_inversion_proj [lemma, in Top.RecordSub]
typing_inversion_rcons [lemma, in Top.RecordSub]
typing_inversion_true [lemma, in Top.Sub]
typing_inversion_unit [lemma, in Top.Sub]
typing_inversion_var [lemma, in Top.Sub]
typing_inversion_var [lemma, in Top.RecordSub]
tzero [constructor, in Top.Types]
T_Abs [constructor, in Top.Norm]
T_Abs [constructor, in Top.RecordSub]
T_Abs [constructor, in Top.Sub]
T_App [constructor, in Top.Sub]
T_App [constructor, in Top.Norm]
T_App [constructor, in Top.RecordSub]
t_empty [definition, in Top.Maps]
T_False [constructor, in Top.Norm]
T_False [constructor, in Top.Sub]
T_False [constructor, in Top.Types]
T_Fst [constructor, in Top.Norm]
T_If [constructor, in Top.Sub]
T_If [constructor, in Top.Types]
T_If [constructor, in Top.Norm]
T_Iszero [constructor, in Top.Types]
T_Pair [constructor, in Top.Norm]
T_Pred [constructor, in Top.Types]
T_Proj [constructor, in Top.RecordSub]
T_RCons [constructor, in Top.RecordSub]
T_RNil [constructor, in Top.RecordSub]
T_Snd [constructor, in Top.Norm]
T_Sub [constructor, in Top.Sub]
T_Sub [constructor, in Top.RecordSub]
T_Succ [constructor, in Top.Types]
T_True [constructor, in Top.Types]
T_True [constructor, in Top.Sub]
T_True [constructor, in Top.Norm]
T_Unit [constructor, in Top.Sub]
t_update [definition, in Top.Maps]
t_update_eq [lemma, in Top.Maps]
t_update_neq [lemma, in Top.Maps]
t_update_permute [lemma, in Top.Maps]
t_update_same [lemma, in Top.Maps]
t_update_shadow [lemma, in Top.Maps]
T_Var [constructor, in Top.RecordSub]
T_Var [constructor, in Top.Norm]
T_Var [constructor, in Top.Sub]
T_Zero [constructor, in Top.Types]
U
UnfoldsExample [module, in Top.UseTactics]UnfoldsExample.bexp_eval_true [lemma, in Top.UseTactics]
Union [constructor, in Top.IndProp]
update [definition, in Top.Maps]
update_eq [lemma, in Top.Maps]
update_example1 [definition, in Top.Maps]
update_example2 [definition, in Top.Maps]
update_example3 [definition, in Top.Maps]
update_example4 [definition, in Top.Maps]
update_neq [lemma, in Top.Maps]
update_permute [lemma, in Top.Maps]
update_same [lemma, in Top.Maps]
update_shadow [lemma, in Top.Maps]
UseAuto [library]
UseTactics [library]
V
vacuous_substitution [lemma, in Top.Norm]value [inductive, in Top.RecordSub]
value [inductive, in Top.Norm]
value [inductive, in Top.Smallstep]
value [inductive, in Top.Sub]
value [definition, in Top.Types]
value_halts [lemma, in Top.Norm]
value_is_nf [lemma, in Top.Types]
value_is_nf [lemma, in Top.Smallstep]
value__normal [lemma, in Top.Norm]
var_not_used_in_aexp [inductive, in Top.Equiv]
verification_conditions [definition, in Top.Hoare2]
verification_correct [lemma, in Top.Hoare2]
VNUId [constructor, in Top.Equiv]
VNUMinus [constructor, in Top.Equiv]
VNUMult [constructor, in Top.Equiv]
VNUNum [constructor, in Top.Equiv]
VNUPlus [constructor, in Top.Equiv]
v_abs [constructor, in Top.Sub]
v_abs [constructor, in Top.Norm]
v_abs [constructor, in Top.RecordSub]
V_cons [constructor, in Top.Norm]
v_const [constructor, in Top.Smallstep]
v_false [constructor, in Top.Norm]
v_false [constructor, in Top.Sub]
V_nil [constructor, in Top.Norm]
v_pair [constructor, in Top.Norm]
v_rcons [constructor, in Top.RecordSub]
v_rnil [constructor, in Top.RecordSub]
v_true [constructor, in Top.Sub]
v_true [constructor, in Top.Norm]
v_unit [constructor, in Top.Sub]
W
wednesday [constructor, in Top.Basics]well_formed_ty [inductive, in Top.RecordSub]
wfTArrow [constructor, in Top.RecordSub]
wfTBase [constructor, in Top.RecordSub]
wfTRCons [constructor, in Top.RecordSub]
wfTRNil [constructor, in Top.RecordSub]
wfTTop [constructor, in Top.RecordSub]
wf_rcd_lookup [lemma, in Top.RecordSub]
while_example [definition, in Top.Hoare]
WHILE_false [lemma, in Top.Equiv]
WHILE_true [lemma, in Top.Equiv]
WHILE_true_nonterm [lemma, in Top.Equiv]
white [constructor, in Top.ImpParser]
working_of_auto_1 [lemma, in Top.UseAuto]
working_of_auto_2 [lemma, in Top.UseAuto]
wp [definition, in Top.HoareAsLogic]
wp_is_precondition [lemma, in Top.HoareAsLogic]
wp_is_weakest [lemma, in Top.HoareAsLogic]
wrong_ev [inductive, in Top.IndProp]
wrong_ev_SS [constructor, in Top.IndProp]
wrong_ev_0 [constructor, in Top.IndProp]
X
X [definition, in Top.Imp]XtimesYinZ [definition, in Top.Imp]
Y
Y [definition, in Top.Imp]yes [constructor, in Top.IndPrinciples]
yesno [inductive, in Top.IndPrinciples]
Z
Z [definition, in Top.Imp]zero_nbeq_plus_1 [lemma, in Top.Basics]
zero_nbeq_S [lemma, in Top.Induction]
zero_not_one [lemma, in Top.Logic]
zero_not_one' [lemma, in Top.Logic]
zero_or_succ [lemma, in Top.Logic]
zprop [definition, in Top.Equiv]
zprop_preserving [lemma, in Top.Equiv]
:
{{'_x_'}}'">:dcom_scope:x_'->>'_'{{'_x_'}}' [notation, in Top.Hoare2]{{'_x_'}}'">:dcom_scope:x_'::='_x_'{{'_x_'}}' [notation, in Top.Hoare2]
:dcom_scope:x_';;'_x [notation, in Top.Hoare2]
{{'_x_'}}'_x_'ELSE'_'{{'_x_'}}'_x_'FI'_'{{'_x_'}}'">:dcom_scope:'IFB'_x_'THEN'_'{{'_x_'}}'_x_'ELSE'_'{{'_x_'}}'_x_'FI'_'{{'_x_'}}' [notation, in Top.Hoare2]
{{'_x_'}}'">:dcom_scope:'SKIP'_'{{'_x_'}}' [notation, in Top.Hoare2]
{{'_x_'}}'_x_'END'_'{{'_x_'}}'">:dcom_scope:'WHILE'_x_'DO'_'{{'_x_'}}'_x_'END'_'{{'_x_'}}' [notation, in Top.Hoare2]
{{'_x_'}}'_x">:dcom_scope:'->>'_'{{'_x_'}}'_x [notation, in Top.Hoare2]
{{'_x_'}}'_x">:dcom_scope:'{{'_x_'}}'_x [notation, in Top.Hoare2]
:hoare_spec_scope:x_'->>'_x [notation, in Top.Hoare]
:hoare_spec_scope:x_'<<->>'_x [notation, in Top.Hoare]
{{'_x_'}}'_x_'{{'_x_'}}'">:hoare_spec_scope:'{{'_x_'}}'_x_'{{'_x_'}}' [notation, in Top.Hoare]
:ltac_scope:'>>' [notation, in Top.LibTactics]
:ltac_scope:'>>'_x [notation, in Top.LibTactics]
:ltac_scope:'>>'_x_x [notation, in Top.LibTactics]
:ltac_scope:'>>'_x_x_x [notation, in Top.LibTactics]
:ltac_scope:'>>'_x_x_x_x [notation, in Top.LibTactics]
:ltac_scope:'>>'_x_x_x_x_x [notation, in Top.LibTactics]
:ltac_scope:'>>'_x_x_x_x_x_x [notation, in Top.LibTactics]
:ltac_scope:'>>'_x_x_x_x_x_x_x [notation, in Top.LibTactics]
:ltac_scope:'>>'_x_x_x_x_x_x_x_x [notation, in Top.LibTactics]
:ltac_scope:'>>'_x_x_x_x_x_x_x_x_x [notation, in Top.LibTactics]
:ltac_scope:'>>'_x_x_x_x_x_x_x_x_x_x [notation, in Top.LibTactics]
:ltac_scope:'>>'_x_x_x_x_x_x_x_x_x_x_x [notation, in Top.LibTactics]
:ltac_scope:'>>'_x_x_x_x_x_x_x_x_x_x_x_x [notation, in Top.LibTactics]
:ltac_scope:'>>'_x_x_x_x_x_x_x_x_x_x_x_x_x [notation, in Top.LibTactics]
:ltac_scope:'__' [notation, in Top.LibTactics]
:ltac_scope:'___' [notation, in Top.LibTactics]
:nat_scope:x_'*'_x [notation, in Top.Basics]
:nat_scope:x_'*'_x [notation, in Top.Basics]
:nat_scope:x_'+'_x [notation, in Top.Basics]
:nat_scope:x_'+'_x [notation, in Top.Basics]
:nat_scope:x_'-'_x [notation, in Top.Basics]
:nat_scope:x_'<=?'_x [notation, in Top.ImpParser]
:type_scope:x_'*'_x [notation, in Top.Poly]
::x_'&&'_x [notation, in Top.Basics]
::x_'++'_x [notation, in Top.Poly]
::x_'/'_x_'/'_x_'\\'_x [notation, in Top.PE]
::x_'/'_x_'==>a'_x [notation, in Top.Smallstep]
::x_'/'_x_'==>a*'_x [notation, in Top.Types]
::x_'/'_x_'==>b'_x [notation, in Top.Smallstep]
::x_'/'_x_'==>'_x_'/'_x [notation, in Top.Smallstep]
::x_'/'_x_'\\'_x [notation, in Top.Imp]
::x_'/'_x_'\\'_x_'/'_x [notation, in Top.PE]
::x_'::'_x [notation, in Top.Poly]
::x_'::='_x [notation, in Top.Imp]
::x_';;'_x [notation, in Top.Imp]
::x_'<'_x [notation, in Top.IndProp]
::x_'<:'_x [notation, in Top.Sub]
::x_'<:'_x [notation, in Top.RecordSub]
::x_'<='_x [notation, in Top.IndPrinciples]
::x_'='''_x [notation, in Top.LibTactics]
::x_'==>'_x [notation, in Top.Sub]
::x_'==>'_x [notation, in Top.Types]
::x_'==>'_x [notation, in Top.Smallstep]
::x_'==>'_x [notation, in Top.Norm]
::x_'==>'_x [notation, in Top.RecordSub]
::x_'==>*'_x [notation, in Top.Types]
::x_'==>*'_x [notation, in Top.Smallstep]
::x_'==>*'_x [notation, in Top.Norm]
::x_'=~'_x [notation, in Top.IndProp]
::x_'['_x_'|->'_x_']' [notation, in Top.Hoare]
::x_'\\'_x [notation, in Top.Smallstep]
::x_'|-'_x_'∈'_x [notation, in Top.Sub]
::x_'|-'_x_'∈'_x [notation, in Top.RecordSub]
::x_'||'_x [notation, in Top.Basics]
::'DO'_'('_x_','_x_')'_'<--'_x_';'_x_'OR'_x [notation, in Top.ImpParser]
::'DO'_'('_x_','_x_')'_'<=='_x_';'_x [notation, in Top.ImpParser]
::'IFB'_x_'THEN'_x_'ELSE'_x_'FI' [notation, in Top.Imp]
::'LETOPT'_x_'<=='_x_'IN'_x [notation, in Top.ImpCEvalFun]
::'nosimpl'_x [notation, in Top.LibTactics]
::'Register'_x_x [notation, in Top.LibTactics]
::'SKIP' [notation, in Top.Imp]
::'Something' [notation, in Top.LibTactics]
::'WHILE'_x_'DO'_x_'END' [notation, in Top.Imp]
::'('_x_','_x_')' [notation, in Top.Poly]
::'['_x_':='_x_']'_x [notation, in Top.RecordSub]
::'['_x_':='_x_']'_x [notation, in Top.Sub]
::'['_x_':='_x_']'_x [notation, in Top.Norm]
::'['_x_';'_'..'_';'_x_']' [notation, in Top.Poly]
::'['_']' [notation, in Top.Poly]
::'|-'_x_'∈'_x [notation, in Top.Types]
Notation Index
A
aevalR_division.:type_scope:x_'\\'_x [in Top.Imp]aevalR_extended.:type_scope:x_'\\'_x [in Top.Imp]
AExp.aevalR_first_try.:type_scope:x_'\\'_x [in Top.Imp]
AExp.:type_scope:x_'\\'_x [in Top.Imp]
B
BreakImp.::x_'/'_x_'\\'_x_'/'_x [in Top.Imp]BreakImp.::x_'::='_x [in Top.Imp]
BreakImp.::x_';;'_x [in Top.Imp]
BreakImp.::'BREAK' [in Top.Imp]
BreakImp.::'IFB'_x_'THEN'_x_'ELSE'_x_'FI' [in Top.Imp]
BreakImp.::'SKIP' [in Top.Imp]
BreakImp.::'WHILE'_x_'DO'_x_'END' [in Top.Imp]
C
CImp.::x_'/'_x_'==>'_x_'/'_x [in Top.Smallstep]CImp.::x_'/'_x_'==>*'_x_'/'_x [in Top.Smallstep]
CImp.::x_'::='_x [in Top.Smallstep]
CImp.::x_';;'_x [in Top.Smallstep]
CImp.::'IFB'_x_'THEN'_x_'ELSE'_x_'FI' [in Top.Smallstep]
CImp.::'PAR'_x_'WITH'_x_'END' [in Top.Smallstep]
CImp.::'SKIP' [in Top.Smallstep]
CImp.::'WHILE'_x_'DO'_x_'END' [in Top.Smallstep]
Combined.::x_'==>'_x [in Top.Smallstep]
H
{{'_x_'}}'_x_'{{'_x_'}}'">Himp.:hoare_spec_scope:'{{'_x_'}}'_x_'{{'_x_'}}' [in Top.Hoare]Himp.::x_'/'_x_'\\'_x [in Top.Hoare]
Himp.::x_'/'_x_'\\'_x [in Top.Equiv]
Himp.::x_'::='_x [in Top.Hoare]
Himp.::x_'::='_x [in Top.Equiv]
Himp.::x_';;'_x [in Top.Hoare]
Himp.::x_';;'_x [in Top.Equiv]
Himp.::'HAVOC'_x [in Top.Hoare]
Himp.::'HAVOC'_x [in Top.Equiv]
Himp.::'IFB'_x_'THEN'_x_'ELSE'_x_'FI' [in Top.Hoare]
Himp.::'IFB'_x_'THEN'_x_'ELSE'_x_'FI' [in Top.Equiv]
Himp.::'SKIP' [in Top.Hoare]
Himp.::'SKIP' [in Top.Equiv]
Himp.::'WHILE'_x_'DO'_x_'END' [in Top.Equiv]
Himp.::'WHILE'_x_'DO'_x_'END' [in Top.Hoare]
I
{{'_x_'}}'_x_'{{'_x_'}}'">If1.:hoare_spec_scope:'{{'_x_'}}'_x_'{{'_x_'}}' [in Top.Hoare]If1.::x_'/'_x_'\\'_x [in Top.Hoare]
If1.::x_'::='_x [in Top.Hoare]
If1.::x_';;'_x [in Top.Hoare]
If1.::'IFB'_x_'THEN'_x_'ELSE'_x_'FI' [in Top.Hoare]
If1.::'IF1'_x_'THEN'_x_'FI' [in Top.Hoare]
If1.::'SKIP' [in Top.Hoare]
If1.::'WHILE'_x_'DO'_x_'END' [in Top.Hoare]
L
LeModule.::x_'<='_x [in Top.IndProp]Loop.::x_'/'_x_'/'_x_'/'_x_'\\'_x_'#'_x [in Top.PE]
Loop.::x_'/'_x_'\\'_x_'#'_x [in Top.PE]
Loop.::x_'/'_x_'\\'_x_'/'_x_'/'_x [in Top.PE]
M
MyEquality.:type_scope:x_'='_x [in Top.ProofObjects]MyIff.:type_scope:x_'<->'_x [in Top.Logic]
MyNot.:type_scope:'~'_x [in Top.Logic]
N
NatList.::x_'++'_x [in Top.Lists]NatList.::x_'::'_x [in Top.Lists]
NatList.::'('_x_','_x_')' [in Top.Lists]
NatList.::'['_x_';'_'..'_';'_x_']' [in Top.Lists]
NatList.::'['_']' [in Top.Lists]
R
RepeatExercise.::x_'/'_x_'\\'_x [in Top.Hoare]RepeatExercise.::x_'::='_x [in Top.Hoare]
RepeatExercise.::x_';;'_x [in Top.Hoare]
RepeatExercise.::'IFB'_x_'THEN'_x_'ELSE'_x_'FI' [in Top.Hoare]
RepeatExercise.::'REPEAT'_x_'UNTIL'_x_'END' [in Top.Hoare]
RepeatExercise.::'SKIP' [in Top.Hoare]
RepeatExercise.::'WHILE'_x_'DO'_x_'END' [in Top.Hoare]
{{'_x_'}}'_x_'{{'_x_'}}'">RepeatExercise.::'{{'_x_'}}'_x_'{{'_x_'}}' [in Top.Hoare]
Repeat.::x_'/'_x_'\\'_x [in Top.Auto]
Repeat.::x_'::='_x [in Top.Auto]
Repeat.::x_';'_x [in Top.Auto]
Repeat.::'IFB'_x_'THEN'_x_'ELSE'_x_'FI' [in Top.Auto]
Repeat.::'REPEAT'_x_'UNTIL'_x_'END' [in Top.Auto]
Repeat.::'SKIP' [in Top.Auto]
Repeat.::'WHILE'_x_'DO'_x_'END' [in Top.Auto]
S
SimpleArith1.::x_'==>'_x [in Top.Smallstep]STLCExtendedRecords.::x_'==>'_x [in Top.Records]
STLCExtendedRecords.::x_'==>*'_x [in Top.Records]
STLCExtendedRecords.::x_'|-'_x_'∈'_x [in Top.Records]
STLCExtendedRecords.::'['_x_':='_x_']'_x [in Top.Records]
STLCExtended.::x_'==>'_x [in Top.MoreStlc]
STLCExtended.::x_'==>*'_x [in Top.MoreStlc]
STLCExtended.::x_'|-'_x_'∈'_x [in Top.MoreStlc]
STLCExtended.::'['_x_':='_x_']'_x [in Top.MoreStlc]
STLCRef.RefsAndNontermination.::x_'/'_x_'==>+'_x_'/'_x [in Top.References]
STLCRef.::x_'/'_x_'==>'_x_'/'_x [in Top.References]
STLCRef.::x_'/'_x_'==>*'_x_'/'_x [in Top.References]
STLCRef.::x_';'_x_'|-'_x_'∈'_x [in Top.References]
STLCRef.::'['_x_':='_x_']'_x [in Top.References]
STLC.::x_'==>'_x [in Top.Stlc]
STLC.::x_'==>*'_x [in Top.Stlc]
STLC.::x_'|-'_x_'∈'_x [in Top.Stlc]
STLC.::'['_x_':='_x_']'_x [in Top.Stlc]
T
Temp1.::x_'==>'_x [in Top.Smallstep]Temp2.::x_'==>'_x [in Top.Smallstep]
Temp3.::x_'==>'_x [in Top.Smallstep]
Temp4.Temp5.::x_'==>'_x [in Top.Smallstep]
Temp4.::x_'==>'_x [in Top.Smallstep]
:
{{'_x_'}}'">:dcom_scope:x_'->>'_'{{'_x_'}}' [in Top.Hoare2]{{'_x_'}}'">:dcom_scope:x_'::='_x_'{{'_x_'}}' [in Top.Hoare2]
:dcom_scope:x_';;'_x [in Top.Hoare2]
{{'_x_'}}'_x_'ELSE'_'{{'_x_'}}'_x_'FI'_'{{'_x_'}}'">:dcom_scope:'IFB'_x_'THEN'_'{{'_x_'}}'_x_'ELSE'_'{{'_x_'}}'_x_'FI'_'{{'_x_'}}' [in Top.Hoare2]
{{'_x_'}}'">:dcom_scope:'SKIP'_'{{'_x_'}}' [in Top.Hoare2]
{{'_x_'}}'_x_'END'_'{{'_x_'}}'">:dcom_scope:'WHILE'_x_'DO'_'{{'_x_'}}'_x_'END'_'{{'_x_'}}' [in Top.Hoare2]
{{'_x_'}}'_x">:dcom_scope:'->>'_'{{'_x_'}}'_x [in Top.Hoare2]
{{'_x_'}}'_x">:dcom_scope:'{{'_x_'}}'_x [in Top.Hoare2]
:hoare_spec_scope:x_'->>'_x [in Top.Hoare]
:hoare_spec_scope:x_'<<->>'_x [in Top.Hoare]
{{'_x_'}}'_x_'{{'_x_'}}'">:hoare_spec_scope:'{{'_x_'}}'_x_'{{'_x_'}}' [in Top.Hoare]
:ltac_scope:'>>' [in Top.LibTactics]
:ltac_scope:'>>'_x [in Top.LibTactics]
:ltac_scope:'>>'_x_x [in Top.LibTactics]
:ltac_scope:'>>'_x_x_x [in Top.LibTactics]
:ltac_scope:'>>'_x_x_x_x [in Top.LibTactics]
:ltac_scope:'>>'_x_x_x_x_x [in Top.LibTactics]
:ltac_scope:'>>'_x_x_x_x_x_x [in Top.LibTactics]
:ltac_scope:'>>'_x_x_x_x_x_x_x [in Top.LibTactics]
:ltac_scope:'>>'_x_x_x_x_x_x_x_x [in Top.LibTactics]
:ltac_scope:'>>'_x_x_x_x_x_x_x_x_x [in Top.LibTactics]
:ltac_scope:'>>'_x_x_x_x_x_x_x_x_x_x [in Top.LibTactics]
:ltac_scope:'>>'_x_x_x_x_x_x_x_x_x_x_x [in Top.LibTactics]
:ltac_scope:'>>'_x_x_x_x_x_x_x_x_x_x_x_x [in Top.LibTactics]
:ltac_scope:'>>'_x_x_x_x_x_x_x_x_x_x_x_x_x [in Top.LibTactics]
:ltac_scope:'__' [in Top.LibTactics]
:ltac_scope:'___' [in Top.LibTactics]
:nat_scope:x_'*'_x [in Top.Basics]
:nat_scope:x_'*'_x [in Top.Basics]
:nat_scope:x_'+'_x [in Top.Basics]
:nat_scope:x_'+'_x [in Top.Basics]
:nat_scope:x_'-'_x [in Top.Basics]
:nat_scope:x_'<=?'_x [in Top.ImpParser]
:type_scope:x_'*'_x [in Top.Poly]
::x_'&&'_x [in Top.Basics]
::x_'++'_x [in Top.Poly]
::x_'/'_x_'/'_x_'\\'_x [in Top.PE]
::x_'/'_x_'==>a'_x [in Top.Smallstep]
::x_'/'_x_'==>a*'_x [in Top.Types]
::x_'/'_x_'==>b'_x [in Top.Smallstep]
::x_'/'_x_'==>'_x_'/'_x [in Top.Smallstep]
::x_'/'_x_'\\'_x [in Top.Imp]
::x_'/'_x_'\\'_x_'/'_x [in Top.PE]
::x_'::'_x [in Top.Poly]
::x_'::='_x [in Top.Imp]
::x_';;'_x [in Top.Imp]
::x_'<'_x [in Top.IndProp]
::x_'<:'_x [in Top.Sub]
::x_'<:'_x [in Top.RecordSub]
::x_'<='_x [in Top.IndPrinciples]
::x_'='''_x [in Top.LibTactics]
::x_'==>'_x [in Top.Sub]
::x_'==>'_x [in Top.Types]
::x_'==>'_x [in Top.Smallstep]
::x_'==>'_x [in Top.Norm]
::x_'==>'_x [in Top.RecordSub]
::x_'==>*'_x [in Top.Types]
::x_'==>*'_x [in Top.Smallstep]
::x_'==>*'_x [in Top.Norm]
::x_'=~'_x [in Top.IndProp]
::x_'['_x_'|->'_x_']' [in Top.Hoare]
::x_'\\'_x [in Top.Smallstep]
::x_'|-'_x_'∈'_x [in Top.Sub]
::x_'|-'_x_'∈'_x [in Top.RecordSub]
::x_'||'_x [in Top.Basics]
::'DO'_'('_x_','_x_')'_'<--'_x_';'_x_'OR'_x [in Top.ImpParser]
::'DO'_'('_x_','_x_')'_'<=='_x_';'_x [in Top.ImpParser]
::'IFB'_x_'THEN'_x_'ELSE'_x_'FI' [in Top.Imp]
::'LETOPT'_x_'<=='_x_'IN'_x [in Top.ImpCEvalFun]
::'nosimpl'_x [in Top.LibTactics]
::'Register'_x_x [in Top.LibTactics]
::'SKIP' [in Top.Imp]
::'Something' [in Top.LibTactics]
::'WHILE'_x_'DO'_x_'END' [in Top.Imp]
::'('_x_','_x_')' [in Top.Poly]
::'['_x_':='_x_']'_x [in Top.RecordSub]
::'['_x_':='_x_']'_x [in Top.Sub]
::'['_x_':='_x_']'_x [in Top.Norm]
::'['_x_';'_'..'_';'_x_']' [in Top.Poly]
::'['_']' [in Top.Poly]
::'|-'_x_'∈'_x [in Top.Types]
Module Index
A
aevalR_division [in Top.Imp]aevalR_extended [in Top.Imp]
AExp [in Top.Imp]
AExp.aevalR_first_try [in Top.Imp]
B
BreakImp [in Top.Imp]C
CImp [in Top.Smallstep]Combined [in Top.Smallstep]
D
DeterministicImp [in Top.UseAuto]E
EqualityExamples [in Top.UseTactics]Examples [in Top.RecordSub]
Examples [in Top.Sub]
ExamplesInstantiations [in Top.UseTactics]
ExamplesLets [in Top.UseTactics]
Examples2 [in Top.RecordSub]
Examples2 [in Top.Sub]
ExAssertions [in Top.Hoare]
Exercises [in Top.Poly]
Exercises.Church [in Top.Poly]
G
GenExample [in Top.UseTactics]H
Himp [in Top.Equiv]Himp [in Top.Hoare]
Himp2 [in Top.Hoare2]
I
If1 [in Top.Hoare]IntrovExamples [in Top.UseTactics]
InvertsExamples [in Top.UseTactics]
L
LeModule [in Top.IndProp]LibTacticsCompatibility [in Top.LibTactics]
Loop [in Top.PE]
M
MumbleGrumble [in Top.Poly]MyEquality [in Top.ProofObjects]
MyIff [in Top.Logic]
MyNot [in Top.Logic]
N
NaryExamples [in Top.UseTactics]NatList [in Top.Lists]
P
PartialMap [in Top.Lists]Playground1 [in Top.Basics]
Playground2 [in Top.Basics]
PreservationProgressReferences [in Top.UseAuto]
PreservationProgressStlc [in Top.UseAuto]
Props [in Top.ProofObjects]
Props.And [in Top.ProofObjects]
Props.Ex [in Top.ProofObjects]
Props.Or [in Top.ProofObjects]
Pumping [in Top.IndProp]
R
R [in Top.IndProp]Repeat [in Top.Auto]
RepeatExercise [in Top.Hoare]
RingDemo [in Top.UseAuto]
S
Semantics [in Top.UseAuto]SimpleArith1 [in Top.Smallstep]
SimpleArith2 [in Top.Smallstep]
SkipExample [in Top.UseTactics]
SortExamples [in Top.UseTactics]
STLC [in Top.Stlc]
STLCArith [in Top.StlcProp]
STLCChecker [in Top.Typechecking]
STLCExtended [in Top.MoreStlc]
STLCExtendedRecords [in Top.Records]
STLCExtendedRecords.FirstTry [in Top.Records]
STLCExtended.Examples [in Top.MoreStlc]
STLCExtended.Examples.FixTest1 [in Top.MoreStlc]
STLCExtended.Examples.FixTest2 [in Top.MoreStlc]
STLCExtended.Examples.FixTest3 [in Top.MoreStlc]
STLCExtended.Examples.FixTest4 [in Top.MoreStlc]
STLCExtended.Examples.LetTest [in Top.MoreStlc]
STLCExtended.Examples.ListTest [in Top.MoreStlc]
STLCExtended.Examples.Numtest [in Top.MoreStlc]
STLCExtended.Examples.Prodtest [in Top.MoreStlc]
STLCExtended.Examples.Sumtest1 [in Top.MoreStlc]
STLCExtended.Examples.Sumtest2 [in Top.MoreStlc]
STLCProp [in Top.StlcProp]
STLCRef [in Top.References]
STLCRef.ExampleVariables [in Top.References]
STLCRef.RefsAndNontermination [in Top.References]
SubtypingInversion [in Top.UseAuto]
T
Temp1 [in Top.Smallstep]Temp2 [in Top.Smallstep]
Temp3 [in Top.Smallstep]
Temp4 [in Top.Smallstep]
Temp4.Temp5 [in Top.Smallstep]
U
UnfoldsExample [in Top.UseTactics]Variable Index
E
equatesLemma.A0 [in Top.LibTactics]equatesLemma.A1 [in Top.LibTactics]
equatesLemma.A2 [in Top.LibTactics]
equatesLemma.A3 [in Top.LibTactics]
equatesLemma.A4 [in Top.LibTactics]
equatesLemma.A5 [in Top.LibTactics]
equatesLemma.A6 [in Top.LibTactics]
S
skip_axiom [in Top.LibTactics]Library Index
A
AutoB
BasicsBib
E
EquivExtraction
H
HoareHoareAsLogic
Hoare2
I
ImpImpCEvalFun
ImpParser
IndPrinciples
IndProp
Induction
L
LibTacticsLists
Logic
M
MapsMoreStlc
N
NormP
PEPoly
Postscript
Preface
ProofObjects
R
RecordsRecordSub
References
Rel
S
SfLibSmallstep
Stlc
StlcProp
Sub
Symbols
T
TacticsTypechecking
Types
U
UseAutoUseTactics
Constructor Index
A
aevalR_division.ADiv [in Top.Imp]aevalR_division.AMinus [in Top.Imp]
aevalR_division.AMult [in Top.Imp]
aevalR_division.ANum [in Top.Imp]
aevalR_division.APlus [in Top.Imp]
aevalR_division.E_ADiv [in Top.Imp]
aevalR_division.E_AMinus [in Top.Imp]
aevalR_division.E_AMult [in Top.Imp]
aevalR_division.E_ANum [in Top.Imp]
aevalR_division.E_APlus [in Top.Imp]
aevalR_extended.AAny [in Top.Imp]
aevalR_extended.AMinus [in Top.Imp]
aevalR_extended.AMult [in Top.Imp]
aevalR_extended.ANum [in Top.Imp]
aevalR_extended.APlus [in Top.Imp]
aevalR_extended.E_AMinus [in Top.Imp]
aevalR_extended.E_AMult [in Top.Imp]
aevalR_extended.E_ANum [in Top.Imp]
aevalR_extended.E_Any [in Top.Imp]
aevalR_extended.E_APlus [in Top.Imp]
AExp.aevalR_first_try.E_AMinus [in Top.Imp]
AExp.aevalR_first_try.E_AMult [in Top.Imp]
AExp.aevalR_first_try.E_ANum [in Top.Imp]
AExp.aevalR_first_try.E_APlus [in Top.Imp]
AExp.AMinus [in Top.Imp]
AExp.AMult [in Top.Imp]
AExp.ANum [in Top.Imp]
AExp.APlus [in Top.Imp]
AExp.BAnd [in Top.Imp]
AExp.BEq [in Top.Imp]
AExp.BFalse [in Top.Imp]
AExp.BLe [in Top.Imp]
AExp.BNot [in Top.Imp]
AExp.BTrue [in Top.Imp]
AExp.E_AMinus [in Top.Imp]
AExp.E_AMult [in Top.Imp]
AExp.E_ANum [in Top.Imp]
AExp.E_APlus [in Top.Imp]
afi_abs [in Top.RecordSub]
afi_abs [in Top.Norm]
afi_abs [in Top.Sub]
afi_app1 [in Top.RecordSub]
afi_app1 [in Top.Norm]
afi_app1 [in Top.Sub]
afi_app2 [in Top.RecordSub]
afi_app2 [in Top.Sub]
afi_app2 [in Top.Norm]
afi_fst [in Top.Norm]
afi_if0 [in Top.Norm]
afi_if1 [in Top.Sub]
afi_if1 [in Top.Norm]
afi_if2 [in Top.Norm]
afi_if2 [in Top.Sub]
afi_if3 [in Top.Sub]
afi_pair1 [in Top.Norm]
afi_pair2 [in Top.Norm]
afi_proj [in Top.RecordSub]
afi_rhead [in Top.RecordSub]
afi_rtail [in Top.RecordSub]
afi_snd [in Top.Norm]
afi_var [in Top.Norm]
afi_var [in Top.Sub]
afi_var [in Top.RecordSub]
AId [in Top.Imp]
alpha [in Top.ImpParser]
AMinus [in Top.Imp]
AMult [in Top.Imp]
ANum [in Top.Imp]
APlus [in Top.Imp]
App [in Top.IndProp]
Assign [in Top.PE]
AS_Id [in Top.Smallstep]
AS_Minus [in Top.Smallstep]
AS_Minus1 [in Top.Smallstep]
AS_Minus2 [in Top.Smallstep]
AS_Mult [in Top.Smallstep]
AS_Mult1 [in Top.Smallstep]
AS_Mult2 [in Top.Smallstep]
AS_Plus [in Top.Smallstep]
AS_Plus1 [in Top.Smallstep]
AS_Plus2 [in Top.Smallstep]
av_num [in Top.Smallstep]
B
BAnd [in Top.Imp]Baz1 [in Top.Lists]
Baz2 [in Top.Lists]
bempty [in Top.IndPrinciples]
BEq [in Top.Imp]
BFalse [in Top.Imp]
BLe [in Top.Imp]
bleaf [in Top.IndPrinciples]
blue [in Top.IndPrinciples]
BNot [in Top.Imp]
body [in Top.PE]
bool_cons [in Top.Poly]
bool_nil [in Top.Poly]
boxer [in Top.LibTactics]
BreakImp.CAss [in Top.Imp]
BreakImp.CBreak [in Top.Imp]
BreakImp.CIf [in Top.Imp]
BreakImp.CSeq [in Top.Imp]
BreakImp.CSkip [in Top.Imp]
BreakImp.CWhile [in Top.Imp]
BreakImp.E_Skip [in Top.Imp]
BreakImp.SBreak [in Top.Imp]
BreakImp.SContinue [in Top.Imp]
BS_AndFalse [in Top.Smallstep]
BS_AndStep [in Top.Smallstep]
BS_AndTrueFalse [in Top.Smallstep]
BS_AndTrueStep [in Top.Smallstep]
BS_AndTrueTrue [in Top.Smallstep]
BS_Eq [in Top.Smallstep]
BS_Eq1 [in Top.Smallstep]
BS_Eq2 [in Top.Smallstep]
BS_LtEq [in Top.Smallstep]
BS_LtEq1 [in Top.Smallstep]
BS_LtEq2 [in Top.Smallstep]
BS_NotFalse [in Top.Smallstep]
BS_NotStep [in Top.Smallstep]
BS_NotTrue [in Top.Smallstep]
BTrue [in Top.Imp]
bv_false [in Top.Types]
bv_true [in Top.Types]
C
C [in Top.Smallstep]CAss [in Top.Imp]
Char [in Top.IndProp]
CIf [in Top.Imp]
CImp.CAss [in Top.Smallstep]
CImp.CIf [in Top.Smallstep]
CImp.CPar [in Top.Smallstep]
CImp.CSeq [in Top.Smallstep]
CImp.CSkip [in Top.Smallstep]
CImp.CS_Ass [in Top.Smallstep]
CImp.CS_AssStep [in Top.Smallstep]
CImp.CS_IfFalse [in Top.Smallstep]
CImp.CS_IfStep [in Top.Smallstep]
CImp.CS_IfTrue [in Top.Smallstep]
CImp.CS_ParDone [in Top.Smallstep]
CImp.CS_Par1 [in Top.Smallstep]
CImp.CS_Par2 [in Top.Smallstep]
CImp.CS_SeqFinish [in Top.Smallstep]
CImp.CS_SeqStep [in Top.Smallstep]
CImp.CS_While [in Top.Smallstep]
CImp.CWhile [in Top.Smallstep]
Combined.C [in Top.Smallstep]
Combined.P [in Top.Smallstep]
Combined.ST_If [in Top.Smallstep]
Combined.ST_IfFalse [in Top.Smallstep]
Combined.ST_IfTrue [in Top.Smallstep]
Combined.ST_PlusConstConst [in Top.Smallstep]
Combined.ST_Plus1 [in Top.Smallstep]
Combined.ST_Plus2 [in Top.Smallstep]
Combined.tfalse [in Top.Smallstep]
Combined.tif [in Top.Smallstep]
Combined.ttrue [in Top.Smallstep]
Combined.v_const [in Top.Smallstep]
Combined.v_false [in Top.Smallstep]
Combined.v_true [in Top.Smallstep]
cons [in Top.Poly]
cons' [in Top.Poly]
CSeq [in Top.Imp]
CSkip [in Top.Imp]
CS_Ass [in Top.Smallstep]
CS_AssStep [in Top.Smallstep]
CS_IfFalse [in Top.Smallstep]
CS_IfStep [in Top.Smallstep]
CS_IfTrue [in Top.Smallstep]
CS_SeqFinish [in Top.Smallstep]
CS_SeqStep [in Top.Smallstep]
CS_While [in Top.Smallstep]
CWhile [in Top.Imp]
C1 [in Top.IndPrinciples]
C2 [in Top.IndPrinciples]
D
DCAsgn [in Top.Hoare2]DCIf [in Top.Hoare2]
DCPost [in Top.Hoare2]
DCPre [in Top.Hoare2]
DCSeq [in Top.Hoare2]
DCSkip [in Top.Hoare2]
DCWhile [in Top.Hoare2]
digit [in Top.ImpParser]
done [in Top.PE]
E
EmptySet [in Top.IndProp]EmptyStr [in Top.IndProp]
entry [in Top.PE]
ev'_sum [in Top.IndProp]
ev'_0 [in Top.IndProp]
ev'_2 [in Top.IndProp]
ev_SS [in Top.Hoare2]
ev_SS [in Top.IndProp]
ev_0 [in Top.IndProp]
ev_0 [in Top.Hoare2]
E_Ass [in Top.Imp]
E_Const [in Top.Smallstep]
E_IfFalse [in Top.Imp]
E_IfTrue [in Top.Imp]
E_None [in Top.PE]
E_Plus [in Top.Smallstep]
E_Seq [in Top.Imp]
E_Skip [in Top.Imp]
E_Some [in Top.PE]
E_WhileEnd [in Top.Imp]
E_WhileLoop [in Top.Imp]
F
false [in Top.Basics]friday [in Top.Basics]
G
Goto [in Top.PE]green [in Top.IndPrinciples]
H
Himp.CAsgn [in Top.Hoare]Himp.CAss [in Top.Equiv]
Himp.CHavoc [in Top.Hoare]
Himp.CHavoc [in Top.Equiv]
Himp.CIf [in Top.Equiv]
Himp.CIf [in Top.Hoare]
Himp.CSeq [in Top.Hoare]
Himp.CSeq [in Top.Equiv]
Himp.CSkip [in Top.Equiv]
Himp.CSkip [in Top.Hoare]
Himp.CWhile [in Top.Hoare]
Himp.CWhile [in Top.Equiv]
Himp.E_Ass [in Top.Equiv]
Himp.E_Ass [in Top.Hoare]
Himp.E_Havoc [in Top.Hoare]
Himp.E_IfFalse [in Top.Equiv]
Himp.E_IfFalse [in Top.Hoare]
Himp.E_IfTrue [in Top.Equiv]
Himp.E_IfTrue [in Top.Hoare]
Himp.E_Seq [in Top.Hoare]
Himp.E_Seq [in Top.Equiv]
Himp.E_Skip [in Top.Equiv]
Himp.E_Skip [in Top.Hoare]
Himp.E_WhileEnd [in Top.Hoare]
Himp.E_WhileEnd [in Top.Equiv]
Himp.E_WhileLoop [in Top.Equiv]
Himp.E_WhileLoop [in Top.Hoare]
H_Asgn [in Top.HoareAsLogic]
H_Consequence [in Top.HoareAsLogic]
H_If [in Top.HoareAsLogic]
H_Seq [in Top.HoareAsLogic]
H_Skip [in Top.HoareAsLogic]
H_While [in Top.HoareAsLogic]
I
Id [in Top.Maps]Id [in Top.Lists]
If [in Top.PE]
If1.CAss [in Top.Hoare]
If1.CIf [in Top.Hoare]
If1.CIf1 [in Top.Hoare]
If1.CSeq [in Top.Hoare]
If1.CSkip [in Top.Hoare]
If1.CWhile [in Top.Hoare]
If1.E_Ass [in Top.Hoare]
If1.E_IfFalse [in Top.Hoare]
If1.E_IfTrue [in Top.Hoare]
If1.E_Seq [in Top.Hoare]
If1.E_Skip [in Top.Hoare]
If1.E_WhileEnd [in Top.Hoare]
If1.E_WhileLoop [in Top.Hoare]
L
leaf [in Top.IndPrinciples]LeModule.le_n [in Top.IndProp]
LeModule.le_S [in Top.IndProp]
le_n [in Top.IndPrinciples]
le_S [in Top.IndPrinciples]
loop [in Top.PE]
Loop.E'Ass [in Top.PE]
Loop.E'IfFalse [in Top.PE]
Loop.E'IfTrue [in Top.PE]
Loop.E'Seq [in Top.PE]
Loop.E'Skip [in Top.PE]
Loop.E'WhileEnd [in Top.PE]
Loop.E'WhileLoop [in Top.PE]
Loop.PE_AssDynamic [in Top.PE]
Loop.PE_AssStatic [in Top.PE]
Loop.pe_ceval_count_intro [in Top.PE]
Loop.PE_If [in Top.PE]
Loop.PE_IfFalse [in Top.PE]
Loop.PE_IfTrue [in Top.PE]
Loop.PE_Seq [in Top.PE]
Loop.PE_Skip [in Top.PE]
Loop.PE_While [in Top.PE]
Loop.PE_WhileEnd [in Top.PE]
Loop.PE_WhileFixed [in Top.PE]
Loop.PE_WhileFixedEnd [in Top.PE]
Loop.PE_WhileFixedLoop [in Top.PE]
Loop.PE_WhileLoop [in Top.PE]
ltac_database_token [in Top.LibTactics]
ltac_mark [in Top.LibTactics]
ltac_no_arg [in Top.LibTactics]
ltac_wild [in Top.LibTactics]
ltac_wilds [in Top.LibTactics]
M
MApp [in Top.IndProp]MChar [in Top.IndProp]
MEmpty [in Top.IndProp]
monday [in Top.Basics]
MStarApp [in Top.IndProp]
MStar0 [in Top.IndProp]
multi_refl [in Top.Smallstep]
multi_step [in Top.Smallstep]
MumbleGrumble.a [in Top.Poly]
MumbleGrumble.b [in Top.Poly]
MumbleGrumble.c [in Top.Poly]
MumbleGrumble.d [in Top.Poly]
MumbleGrumble.e [in Top.Poly]
MUnionL [in Top.IndProp]
MUnionR [in Top.IndProp]
MyEquality.eq_refl [in Top.ProofObjects]
N
NatList.cons [in Top.Lists]NatList.nil [in Top.Lists]
NatList.None [in Top.Lists]
NatList.pair [in Top.Lists]
NatList.Some [in Top.Lists]
nbranch [in Top.IndPrinciples]
ncons [in Top.IndPrinciples]
ne_1 [in Top.IndProp]
ne_2 [in Top.IndProp]
nil [in Top.Poly]
nil' [in Top.Poly]
nn [in Top.IndProp]
nnil [in Top.IndPrinciples]
nnil1 [in Top.IndPrinciples]
no [in Top.IndPrinciples]
node [in Top.IndPrinciples]
None [in Top.Poly]
NoneE [in Top.ImpParser]
nsnoc1 [in Top.IndPrinciples]
nv_succ [in Top.Types]
nv_zero [in Top.Types]
O
other [in Top.ImpParser]P
P [in Top.Smallstep]pair [in Top.Poly]
PartialMap.empty [in Top.Lists]
PartialMap.record [in Top.Lists]
PE_AssDynamic [in Top.PE]
PE_AssStatic [in Top.PE]
pe_ceval_intro [in Top.PE]
PE_If [in Top.PE]
PE_IfFalse [in Top.PE]
PE_IfTrue [in Top.PE]
pe_peval_intro [in Top.PE]
PE_Seq [in Top.PE]
PE_Skip [in Top.PE]
Playground1.O [in Top.Basics]
Playground1.S [in Top.Basics]
Props.And.conj [in Top.ProofObjects]
Props.Ex.ex_intro [in Top.ProofObjects]
Props.I [in Top.ProofObjects]
Props.Or.or_introl [in Top.ProofObjects]
Props.Or.or_intror [in Top.ProofObjects]
R
red [in Top.IndPrinciples]ReflectF [in Top.IndProp]
ReflectT [in Top.IndProp]
RepeatExercise.CAsgn [in Top.Hoare]
RepeatExercise.CIf [in Top.Hoare]
RepeatExercise.CRepeat [in Top.Hoare]
RepeatExercise.CSeq [in Top.Hoare]
RepeatExercise.CSkip [in Top.Hoare]
RepeatExercise.CWhile [in Top.Hoare]
RepeatExercise.E_Ass [in Top.Hoare]
RepeatExercise.E_IfFalse [in Top.Hoare]
RepeatExercise.E_IfTrue [in Top.Hoare]
RepeatExercise.E_Seq [in Top.Hoare]
RepeatExercise.E_Skip [in Top.Hoare]
RepeatExercise.E_WhileEnd [in Top.Hoare]
RepeatExercise.E_WhileLoop [in Top.Hoare]
Repeat.CAsgn [in Top.Auto]
Repeat.CIf [in Top.Auto]
Repeat.CRepeat [in Top.Auto]
Repeat.CSeq [in Top.Auto]
Repeat.CSkip [in Top.Auto]
Repeat.CWhile [in Top.Auto]
Repeat.E_Ass [in Top.Auto]
Repeat.E_IfFalse [in Top.Auto]
Repeat.E_IfTrue [in Top.Auto]
Repeat.E_RepeatEnd [in Top.Auto]
Repeat.E_RepeatLoop [in Top.Auto]
Repeat.E_Seq [in Top.Auto]
Repeat.E_Skip [in Top.Auto]
Repeat.E_WhileEnd [in Top.Auto]
Repeat.E_WhileLoop [in Top.Auto]
RTcons [in Top.RecordSub]
rtcons [in Top.RecordSub]
RTnil [in Top.RecordSub]
rtnil [in Top.RecordSub]
rt1n_refl [in Top.Rel]
rt1n_trans [in Top.Rel]
rt_refl [in Top.Rel]
rt_step [in Top.Rel]
rt_trans [in Top.Rel]
R.c1 [in Top.IndProp]
R.c2 [in Top.IndProp]
R.c3 [in Top.IndProp]
R.c4 [in Top.IndProp]
R.c5 [in Top.IndProp]
S
saturday [in Top.Basics]SimpleArith1.ST_PlusConstConst [in Top.Smallstep]
SimpleArith1.ST_Plus1 [in Top.Smallstep]
SimpleArith1.ST_Plus2 [in Top.Smallstep]
SLoad [in Top.Imp]
SMinus [in Top.Imp]
SMult [in Top.Imp]
Some [in Top.Poly]
SomeE [in Top.ImpParser]
SPlus [in Top.Imp]
SPush [in Top.Imp]
sq [in Top.IndProp]
SS_Load [in Top.Smallstep]
SS_Minus [in Top.Smallstep]
SS_Mult [in Top.Smallstep]
SS_Plus [in Top.Smallstep]
SS_Push [in Top.Smallstep]
Star [in Top.IndProp]
STLCArith.tabs [in Top.StlcProp]
STLCArith.tapp [in Top.StlcProp]
STLCArith.TArrow [in Top.StlcProp]
STLCArith.tif0 [in Top.StlcProp]
STLCArith.tmult [in Top.StlcProp]
STLCArith.tnat [in Top.StlcProp]
STLCArith.TNat [in Top.StlcProp]
STLCArith.tpred [in Top.StlcProp]
STLCArith.tsucc [in Top.StlcProp]
STLCArith.tvar [in Top.StlcProp]
STLCExtendedRecords.afi_abs [in Top.Records]
STLCExtendedRecords.afi_app1 [in Top.Records]
STLCExtendedRecords.afi_app2 [in Top.Records]
STLCExtendedRecords.afi_proj [in Top.Records]
STLCExtendedRecords.afi_rhead [in Top.Records]
STLCExtendedRecords.afi_rtail [in Top.Records]
STLCExtendedRecords.afi_var [in Top.Records]
STLCExtendedRecords.FirstTry.TArrow [in Top.Records]
STLCExtendedRecords.FirstTry.TBase [in Top.Records]
STLCExtendedRecords.FirstTry.TRcd [in Top.Records]
STLCExtendedRecords.rtcons [in Top.Records]
STLCExtendedRecords.RTcons [in Top.Records]
STLCExtendedRecords.rtnil [in Top.Records]
STLCExtendedRecords.RTnil [in Top.Records]
STLCExtendedRecords.ST_AppAbs [in Top.Records]
STLCExtendedRecords.ST_App1 [in Top.Records]
STLCExtendedRecords.ST_App2 [in Top.Records]
STLCExtendedRecords.ST_ProjRcd [in Top.Records]
STLCExtendedRecords.ST_Proj1 [in Top.Records]
STLCExtendedRecords.ST_Rcd_Head [in Top.Records]
STLCExtendedRecords.ST_Rcd_Tail [in Top.Records]
STLCExtendedRecords.tabs [in Top.Records]
STLCExtendedRecords.tapp [in Top.Records]
STLCExtendedRecords.TArrow [in Top.Records]
STLCExtendedRecords.TBase [in Top.Records]
STLCExtendedRecords.tproj [in Top.Records]
STLCExtendedRecords.TRCons [in Top.Records]
STLCExtendedRecords.trcons [in Top.Records]
STLCExtendedRecords.trnil [in Top.Records]
STLCExtendedRecords.TRNil [in Top.Records]
STLCExtendedRecords.tvar [in Top.Records]
STLCExtendedRecords.T_Abs [in Top.Records]
STLCExtendedRecords.T_App [in Top.Records]
STLCExtendedRecords.T_Proj [in Top.Records]
STLCExtendedRecords.T_RCons [in Top.Records]
STLCExtendedRecords.T_RNil [in Top.Records]
STLCExtendedRecords.T_Var [in Top.Records]
STLCExtendedRecords.v_abs [in Top.Records]
STLCExtendedRecords.v_rcons [in Top.Records]
STLCExtendedRecords.v_rnil [in Top.Records]
STLCExtendedRecords.wfTArrow [in Top.Records]
STLCExtendedRecords.wfTBase [in Top.Records]
STLCExtendedRecords.wfTRCons [in Top.Records]
STLCExtendedRecords.wfTRNil [in Top.Records]
STLCExtended.afi_abs [in Top.MoreStlc]
STLCExtended.afi_app1 [in Top.MoreStlc]
STLCExtended.afi_app2 [in Top.MoreStlc]
STLCExtended.afi_case0 [in Top.MoreStlc]
STLCExtended.afi_case1 [in Top.MoreStlc]
STLCExtended.afi_case2 [in Top.MoreStlc]
STLCExtended.afi_cons1 [in Top.MoreStlc]
STLCExtended.afi_cons2 [in Top.MoreStlc]
STLCExtended.afi_fst [in Top.MoreStlc]
STLCExtended.afi_if01 [in Top.MoreStlc]
STLCExtended.afi_if02 [in Top.MoreStlc]
STLCExtended.afi_if03 [in Top.MoreStlc]
STLCExtended.afi_inl [in Top.MoreStlc]
STLCExtended.afi_inr [in Top.MoreStlc]
STLCExtended.afi_lcase1 [in Top.MoreStlc]
STLCExtended.afi_lcase2 [in Top.MoreStlc]
STLCExtended.afi_lcase3 [in Top.MoreStlc]
STLCExtended.afi_mult1 [in Top.MoreStlc]
STLCExtended.afi_mult2 [in Top.MoreStlc]
STLCExtended.afi_pair1 [in Top.MoreStlc]
STLCExtended.afi_pair2 [in Top.MoreStlc]
STLCExtended.afi_pred [in Top.MoreStlc]
STLCExtended.afi_snd [in Top.MoreStlc]
STLCExtended.afi_succ [in Top.MoreStlc]
STLCExtended.afi_var [in Top.MoreStlc]
STLCExtended.ST_AppAbs [in Top.MoreStlc]
STLCExtended.ST_App1 [in Top.MoreStlc]
STLCExtended.ST_App2 [in Top.MoreStlc]
STLCExtended.ST_Case [in Top.MoreStlc]
STLCExtended.ST_CaseInl [in Top.MoreStlc]
STLCExtended.ST_CaseInr [in Top.MoreStlc]
STLCExtended.ST_Cons1 [in Top.MoreStlc]
STLCExtended.ST_Cons2 [in Top.MoreStlc]
STLCExtended.ST_FstPair [in Top.MoreStlc]
STLCExtended.ST_Fst1 [in Top.MoreStlc]
STLCExtended.ST_If0Nonzero [in Top.MoreStlc]
STLCExtended.ST_If0Zero [in Top.MoreStlc]
STLCExtended.ST_If01 [in Top.MoreStlc]
STLCExtended.ST_Inl [in Top.MoreStlc]
STLCExtended.ST_Inr [in Top.MoreStlc]
STLCExtended.ST_LcaseCons [in Top.MoreStlc]
STLCExtended.ST_LcaseNil [in Top.MoreStlc]
STLCExtended.ST_Lcase1 [in Top.MoreStlc]
STLCExtended.ST_MultNats [in Top.MoreStlc]
STLCExtended.ST_Mult1 [in Top.MoreStlc]
STLCExtended.ST_Mult2 [in Top.MoreStlc]
STLCExtended.ST_Pair1 [in Top.MoreStlc]
STLCExtended.ST_Pair2 [in Top.MoreStlc]
STLCExtended.ST_Pred [in Top.MoreStlc]
STLCExtended.ST_PredNat [in Top.MoreStlc]
STLCExtended.ST_SndPair [in Top.MoreStlc]
STLCExtended.ST_Snd1 [in Top.MoreStlc]
STLCExtended.ST_SuccNat [in Top.MoreStlc]
STLCExtended.ST_Succ1 [in Top.MoreStlc]
STLCExtended.tabs [in Top.MoreStlc]
STLCExtended.tapp [in Top.MoreStlc]
STLCExtended.TArrow [in Top.MoreStlc]
STLCExtended.tcase [in Top.MoreStlc]
STLCExtended.tcons [in Top.MoreStlc]
STLCExtended.tfix [in Top.MoreStlc]
STLCExtended.tfst [in Top.MoreStlc]
STLCExtended.tif0 [in Top.MoreStlc]
STLCExtended.tinl [in Top.MoreStlc]
STLCExtended.tinr [in Top.MoreStlc]
STLCExtended.tlcase [in Top.MoreStlc]
STLCExtended.tlet [in Top.MoreStlc]
STLCExtended.TList [in Top.MoreStlc]
STLCExtended.tmult [in Top.MoreStlc]
STLCExtended.tnat [in Top.MoreStlc]
STLCExtended.TNat [in Top.MoreStlc]
STLCExtended.tnil [in Top.MoreStlc]
STLCExtended.tpair [in Top.MoreStlc]
STLCExtended.tpred [in Top.MoreStlc]
STLCExtended.TProd [in Top.MoreStlc]
STLCExtended.tsnd [in Top.MoreStlc]
STLCExtended.tsucc [in Top.MoreStlc]
STLCExtended.TSum [in Top.MoreStlc]
STLCExtended.TUnit [in Top.MoreStlc]
STLCExtended.tunit [in Top.MoreStlc]
STLCExtended.tvar [in Top.MoreStlc]
STLCExtended.T_Abs [in Top.MoreStlc]
STLCExtended.T_App [in Top.MoreStlc]
STLCExtended.T_Case [in Top.MoreStlc]
STLCExtended.T_Cons [in Top.MoreStlc]
STLCExtended.T_Fst [in Top.MoreStlc]
STLCExtended.T_If0 [in Top.MoreStlc]
STLCExtended.T_Inl [in Top.MoreStlc]
STLCExtended.T_Inr [in Top.MoreStlc]
STLCExtended.T_Lcase [in Top.MoreStlc]
STLCExtended.T_Mult [in Top.MoreStlc]
STLCExtended.T_Nat [in Top.MoreStlc]
STLCExtended.T_Nil [in Top.MoreStlc]
STLCExtended.T_Pair [in Top.MoreStlc]
STLCExtended.T_Pred [in Top.MoreStlc]
STLCExtended.T_Snd [in Top.MoreStlc]
STLCExtended.T_Succ [in Top.MoreStlc]
STLCExtended.T_Unit [in Top.MoreStlc]
STLCExtended.T_Var [in Top.MoreStlc]
STLCExtended.v_abs [in Top.MoreStlc]
STLCExtended.v_inl [in Top.MoreStlc]
STLCExtended.v_inr [in Top.MoreStlc]
STLCExtended.v_lcons [in Top.MoreStlc]
STLCExtended.v_lnil [in Top.MoreStlc]
STLCExtended.v_nat [in Top.MoreStlc]
STLCExtended.v_pair [in Top.MoreStlc]
STLCExtended.v_unit [in Top.MoreStlc]
STLCProp.afi_abs [in Top.StlcProp]
STLCProp.afi_app1 [in Top.StlcProp]
STLCProp.afi_app2 [in Top.StlcProp]
STLCProp.afi_if1 [in Top.StlcProp]
STLCProp.afi_if2 [in Top.StlcProp]
STLCProp.afi_if3 [in Top.StlcProp]
STLCProp.afi_var [in Top.StlcProp]
STLCRef.afi_abs [in Top.References]
STLCRef.afi_app1 [in Top.References]
STLCRef.afi_app2 [in Top.References]
STLCRef.afi_assign1 [in Top.References]
STLCRef.afi_assign2 [in Top.References]
STLCRef.afi_deref [in Top.References]
STLCRef.afi_if0_1 [in Top.References]
STLCRef.afi_if0_2 [in Top.References]
STLCRef.afi_if0_3 [in Top.References]
STLCRef.afi_mult1 [in Top.References]
STLCRef.afi_mult2 [in Top.References]
STLCRef.afi_pred [in Top.References]
STLCRef.afi_ref [in Top.References]
STLCRef.afi_succ [in Top.References]
STLCRef.afi_var [in Top.References]
STLCRef.extends_cons [in Top.References]
STLCRef.extends_nil [in Top.References]
STLCRef.RefsAndNontermination.sc_one [in Top.References]
STLCRef.RefsAndNontermination.sc_step [in Top.References]
STLCRef.ST_AppAbs [in Top.References]
STLCRef.ST_App1 [in Top.References]
STLCRef.ST_App2 [in Top.References]
STLCRef.ST_Assign [in Top.References]
STLCRef.ST_Assign1 [in Top.References]
STLCRef.ST_Assign2 [in Top.References]
STLCRef.ST_Deref [in Top.References]
STLCRef.ST_DerefLoc [in Top.References]
STLCRef.ST_If0 [in Top.References]
STLCRef.ST_If0_Nonzero [in Top.References]
STLCRef.ST_If0_Zero [in Top.References]
STLCRef.ST_MultNats [in Top.References]
STLCRef.ST_Mult1 [in Top.References]
STLCRef.ST_Mult2 [in Top.References]
STLCRef.ST_Pred [in Top.References]
STLCRef.ST_PredNat [in Top.References]
STLCRef.ST_Ref [in Top.References]
STLCRef.ST_RefValue [in Top.References]
STLCRef.ST_Succ [in Top.References]
STLCRef.ST_SuccNat [in Top.References]
STLCRef.tabs [in Top.References]
STLCRef.tapp [in Top.References]
STLCRef.TArrow [in Top.References]
STLCRef.tassign [in Top.References]
STLCRef.tderef [in Top.References]
STLCRef.tif0 [in Top.References]
STLCRef.tloc [in Top.References]
STLCRef.tmult [in Top.References]
STLCRef.TNat [in Top.References]
STLCRef.tnat [in Top.References]
STLCRef.tpred [in Top.References]
STLCRef.tref [in Top.References]
STLCRef.TRef [in Top.References]
STLCRef.tsucc [in Top.References]
STLCRef.tunit [in Top.References]
STLCRef.TUnit [in Top.References]
STLCRef.tvar [in Top.References]
STLCRef.T_Abs [in Top.References]
STLCRef.T_App [in Top.References]
STLCRef.T_Assign [in Top.References]
STLCRef.T_Deref [in Top.References]
STLCRef.T_If0 [in Top.References]
STLCRef.T_Loc [in Top.References]
STLCRef.T_Mult [in Top.References]
STLCRef.T_Nat [in Top.References]
STLCRef.T_Pred [in Top.References]
STLCRef.T_Ref [in Top.References]
STLCRef.T_Succ [in Top.References]
STLCRef.T_Unit [in Top.References]
STLCRef.T_Var [in Top.References]
STLCRef.v_abs [in Top.References]
STLCRef.v_loc [in Top.References]
STLCRef.v_nat [in Top.References]
STLCRef.v_unit [in Top.References]
STLC.ST_AppAbs [in Top.Stlc]
STLC.ST_App1 [in Top.Stlc]
STLC.ST_App2 [in Top.Stlc]
STLC.ST_If [in Top.Stlc]
STLC.ST_IfFalse [in Top.Stlc]
STLC.ST_IfTrue [in Top.Stlc]
STLC.s_var1 [in Top.Stlc]
STLC.tabs [in Top.Stlc]
STLC.tapp [in Top.Stlc]
STLC.TArrow [in Top.Stlc]
STLC.TBool [in Top.Stlc]
STLC.tfalse [in Top.Stlc]
STLC.tif [in Top.Stlc]
STLC.ttrue [in Top.Stlc]
STLC.tvar [in Top.Stlc]
STLC.T_Abs [in Top.Stlc]
STLC.T_App [in Top.Stlc]
STLC.T_False [in Top.Stlc]
STLC.T_If [in Top.Stlc]
STLC.T_True [in Top.Stlc]
STLC.T_Var [in Top.Stlc]
STLC.v_abs [in Top.Stlc]
STLC.v_false [in Top.Stlc]
STLC.v_true [in Top.Stlc]
ST_AppAbs [in Top.RecordSub]
ST_AppAbs [in Top.Sub]
ST_AppAbs [in Top.Norm]
ST_App1 [in Top.RecordSub]
ST_App1 [in Top.Sub]
ST_App1 [in Top.Norm]
ST_App2 [in Top.RecordSub]
ST_App2 [in Top.Norm]
ST_App2 [in Top.Sub]
ST_Fst [in Top.Norm]
ST_FstPair [in Top.Norm]
ST_If [in Top.Norm]
ST_If [in Top.Types]
ST_If [in Top.Sub]
ST_IfFalse [in Top.Types]
ST_IfFalse [in Top.Sub]
ST_IfFalse [in Top.Norm]
ST_IfTrue [in Top.Sub]
ST_IfTrue [in Top.Norm]
ST_IfTrue [in Top.Types]
ST_Iszero [in Top.Types]
ST_IszeroSucc [in Top.Types]
ST_IszeroZero [in Top.Types]
ST_Pair1 [in Top.Norm]
ST_Pair2 [in Top.Norm]
ST_PlusConstConst [in Top.Smallstep]
ST_Plus1 [in Top.Smallstep]
ST_Plus2 [in Top.Smallstep]
ST_Pred [in Top.Types]
ST_PredSucc [in Top.Types]
ST_PredZero [in Top.Types]
ST_ProjRcd [in Top.RecordSub]
ST_Proj1 [in Top.RecordSub]
ST_Rcd_Head [in Top.RecordSub]
ST_Rcd_Tail [in Top.RecordSub]
ST_Snd [in Top.Norm]
ST_SndPair [in Top.Norm]
ST_Succ [in Top.Types]
sunday [in Top.Basics]
S_Arrow [in Top.RecordSub]
S_Arrow [in Top.Sub]
S_RcdDepth [in Top.RecordSub]
S_RcdPerm [in Top.RecordSub]
S_RcdWidth [in Top.RecordSub]
S_Refl [in Top.Sub]
S_Refl [in Top.RecordSub]
S_Top [in Top.RecordSub]
S_Top [in Top.Sub]
S_Trans [in Top.Sub]
S_Trans [in Top.RecordSub]
T
tabs [in Top.Sub]tabs [in Top.RecordSub]
tabs [in Top.Norm]
tapp [in Top.Norm]
tapp [in Top.Sub]
tapp [in Top.RecordSub]
TArrow [in Top.RecordSub]
TArrow [in Top.Norm]
TArrow [in Top.Sub]
TBase [in Top.RecordSub]
TBase [in Top.Sub]
TBool [in Top.Sub]
TBool [in Top.Norm]
TBool [in Top.Types]
Temp1.ST_PlusConstConst [in Top.Smallstep]
Temp1.ST_Plus1 [in Top.Smallstep]
Temp1.ST_Plus2 [in Top.Smallstep]
Temp1.v_const [in Top.Smallstep]
Temp1.v_funny [in Top.Smallstep]
Temp2.ST_Funny [in Top.Smallstep]
Temp2.ST_PlusConstConst [in Top.Smallstep]
Temp2.ST_Plus1 [in Top.Smallstep]
Temp2.ST_Plus2 [in Top.Smallstep]
Temp2.v_const [in Top.Smallstep]
Temp3.ST_PlusConstConst [in Top.Smallstep]
Temp3.ST_Plus1 [in Top.Smallstep]
Temp3.v_const [in Top.Smallstep]
Temp4.ST_If [in Top.Smallstep]
Temp4.ST_IfFalse [in Top.Smallstep]
Temp4.ST_IfTrue [in Top.Smallstep]
Temp4.Temp5.ST_If [in Top.Smallstep]
Temp4.Temp5.ST_IfFalse [in Top.Smallstep]
Temp4.Temp5.ST_IfTrue [in Top.Smallstep]
Temp4.tfalse [in Top.Smallstep]
Temp4.tif [in Top.Smallstep]
Temp4.ttrue [in Top.Smallstep]
Temp4.v_false [in Top.Smallstep]
Temp4.v_true [in Top.Smallstep]
tfalse [in Top.Norm]
tfalse [in Top.Types]
tfalse [in Top.Sub]
tfst [in Top.Norm]
thursday [in Top.Basics]
tif [in Top.Types]
tif [in Top.Norm]
tif [in Top.Sub]
tiszero [in Top.Types]
TNat [in Top.Types]
tpair [in Top.Norm]
tpred [in Top.Types]
TProd [in Top.Norm]
tproj [in Top.RecordSub]
TRCons [in Top.RecordSub]
trcons [in Top.RecordSub]
trnil [in Top.RecordSub]
TRNil [in Top.RecordSub]
true [in Top.Basics]
tsnd [in Top.Norm]
tsucc [in Top.Types]
TTop [in Top.RecordSub]
TTop [in Top.Sub]
ttrue [in Top.Sub]
ttrue [in Top.Norm]
ttrue [in Top.Types]
tuesday [in Top.Basics]
tunit [in Top.Sub]
TUnit [in Top.Sub]
tvar [in Top.Sub]
tvar [in Top.Norm]
tvar [in Top.RecordSub]
tzero [in Top.Types]
T_Abs [in Top.Norm]
T_Abs [in Top.RecordSub]
T_Abs [in Top.Sub]
T_App [in Top.Sub]
T_App [in Top.Norm]
T_App [in Top.RecordSub]
T_False [in Top.Norm]
T_False [in Top.Sub]
T_False [in Top.Types]
T_Fst [in Top.Norm]
T_If [in Top.Sub]
T_If [in Top.Types]
T_If [in Top.Norm]
T_Iszero [in Top.Types]
T_Pair [in Top.Norm]
T_Pred [in Top.Types]
T_Proj [in Top.RecordSub]
T_RCons [in Top.RecordSub]
T_RNil [in Top.RecordSub]
T_Snd [in Top.Norm]
T_Sub [in Top.Sub]
T_Sub [in Top.RecordSub]
T_Succ [in Top.Types]
T_True [in Top.Types]
T_True [in Top.Sub]
T_True [in Top.Norm]
T_Unit [in Top.Sub]
T_Var [in Top.RecordSub]
T_Var [in Top.Norm]
T_Var [in Top.Sub]
T_Zero [in Top.Types]
U
Union [in Top.IndProp]V
VNUId [in Top.Equiv]VNUMinus [in Top.Equiv]
VNUMult [in Top.Equiv]
VNUNum [in Top.Equiv]
VNUPlus [in Top.Equiv]
v_abs [in Top.Sub]
v_abs [in Top.Norm]
v_abs [in Top.RecordSub]
V_cons [in Top.Norm]
v_const [in Top.Smallstep]
v_false [in Top.Norm]
v_false [in Top.Sub]
V_nil [in Top.Norm]
v_pair [in Top.Norm]
v_rcons [in Top.RecordSub]
v_rnil [in Top.RecordSub]
v_true [in Top.Sub]
v_true [in Top.Norm]
v_unit [in Top.Sub]
W
wednesday [in Top.Basics]wfTArrow [in Top.RecordSub]
wfTBase [in Top.RecordSub]
wfTRCons [in Top.RecordSub]
wfTRNil [in Top.RecordSub]
wfTTop [in Top.RecordSub]
white [in Top.ImpParser]
wrong_ev_SS [in Top.IndProp]
wrong_ev_0 [in Top.IndProp]
Y
yes [in Top.IndPrinciples]Lemma Index
A
abs_arrow [in Top.Sub]abs_arrow [in Top.RecordSub]
aequiv_example [in Top.Equiv]
aeval_weakening [in Top.Equiv]
AExp.aeval_iff_aevalR [in Top.Imp]
AExp.aeval_iff_aevalR' [in Top.Imp]
AExp.foo [in Top.Imp]
AExp.foo' [in Top.Imp]
AExp.In10 [in Top.Imp]
AExp.In10' [in Top.Imp]
AExp.optimize_0plus_b_sound [in Top.Imp]
AExp.optimize_0plus_sound [in Top.Imp]
AExp.optimize_0plus_sound' [in Top.Imp]
AExp.optimize_0plus_sound'' [in Top.Imp]
AExp.silly1 [in Top.Imp]
AExp.silly2 [in Top.Imp]
all3_spec [in Top.Induction]
All_In [in Top.Logic]
always_loop_hoare [in Top.Hoare]
andb3_exchange [in Top.Basics]
andb_commutative [in Top.Basics]
andb_commutative' [in Top.Basics]
andb_commutative'' [in Top.Basics]
andb_eq_orb [in Top.Basics]
andb_false_r [in Top.Induction]
andb_true_elim2 [in Top.Basics]
andb_true_iff [in Top.Logic]
and_assoc [in Top.Logic]
and_commut [in Top.Logic]
and_example2 [in Top.Logic]
and_example2' [in Top.Logic]
and_example2'' [in Top.Logic]
and_example3 [in Top.Logic]
and_intro [in Top.Logic]
apply_iff_example [in Top.Logic]
app_assoc [in Top.Poly]
app_length [in Top.Poly]
app_length_cons [in Top.Tactics]
app_length_twice [in Top.Tactics]
app_nil_r [in Top.Poly]
assign_aequiv [in Top.Equiv]
assign_removes [in Top.PE]
B
bassn_eval_false [in Top.HoareAsLogic]bequiv_example [in Top.Equiv]
beq_idP [in Top.Maps]
beq_id_false_iff [in Top.Maps]
beq_id_refl [in Top.Lists]
beq_id_refl [in Top.Maps]
beq_id_true [in Top.Tactics]
beq_id_true_iff [in Top.Maps]
beq_list_true_iff [in Top.Logic]
beq_natP [in Top.IndProp]
beq_nat_false_iff [in Top.Logic]
beq_nat_refl [in Top.Induction]
beq_nat_sym [in Top.Tactics]
beq_nat_trans [in Top.Tactics]
beq_nat_true [in Top.Tactics]
beq_nat_true_iff [in Top.Logic]
beq_nat_0_l [in Top.Tactics]
bexp_eval_false [in Top.Hoare]
bexp_eval_true [in Top.Hoare]
bool_canonical [in Top.Types]
bool_fn_applied_thrice [in Top.Tactics]
BreakImp.break_ignore [in Top.Imp]
BreakImp.ceval_deterministic [in Top.Imp]
BreakImp.while_break_true [in Top.Imp]
BreakImp.while_continue [in Top.Imp]
BreakImp.while_stops_on_break [in Top.Imp]
C
canonical_forms_of_arrow_types [in Top.RecordSub]canonical_forms_of_arrow_types [in Top.Sub]
canonical_forms_of_Bool [in Top.Sub]
CAss_congruence [in Top.Equiv]
ceval_and_ceval_step_coincide [in Top.ImpCEvalFun]
ceval_deterministic [in Top.Imp]
ceval_deterministic [in Top.Auto]
ceval_deterministic' [in Top.Auto]
ceval_deterministic' [in Top.ImpCEvalFun]
ceval_deterministic'' [in Top.Auto]
ceval_deterministic''' [in Top.Auto]
ceval_deterministic'''' [in Top.Auto]
ceval_deterministic''''' [in Top.Auto]
ceval_deterministic'_alt [in Top.Auto]
ceval_extensionality [in Top.PE]
ceval_step_more [in Top.ImpCEvalFun]
ceval_step__ceval [in Top.ImpCEvalFun]
ceval__ceval_step [in Top.ImpCEvalFun]
CIf_congruence [in Top.Equiv]
CImp.par_body_n [in Top.Smallstep]
CImp.par_body_n__Sn [in Top.Smallstep]
CImp.par_loop_any_X [in Top.Smallstep]
cmin_minimal [in Top.Equiv]
combine_odd_even_elim_even [in Top.Logic]
combine_odd_even_elim_odd [in Top.Logic]
combine_odd_even_intro [in Top.Logic]
combine_split [in Top.Tactics]
compiler_is_correct [in Top.Smallstep]
congruence_demo_1 [in Top.UseAuto]
congruence_demo_2 [in Top.UseAuto]
congruence_demo_3 [in Top.UseAuto]
congruence_demo_4 [in Top.UseAuto]
context_invariance [in Top.RecordSub]
context_invariance [in Top.Norm]
context_invariance [in Top.Sub]
contradiction_implies_anything [in Top.Logic]
contrapositive [in Top.Logic]
CSeq_congruence [in Top.Equiv]
CWhile_congruence [in Top.Equiv]
c3_c4_different [in Top.Equiv]
D
dec_while_correct [in Top.Hoare2]demo_auto_absurd_1 [in Top.UseAuto]
demo_auto_absurd_2 [in Top.UseAuto]
demo_clears_all_and_clears_but [in Top.LibTactics]
demo_false [in Top.UseTactics]
demo_false [in Top.UseAuto]
demo_false_arg [in Top.UseTactics]
demo_hint_unfold_context_1 [in Top.UseAuto]
demo_hint_unfold_context_2 [in Top.UseAuto]
demo_hint_unfold_goal_1 [in Top.UseAuto]
demo_hint_unfold_goal_2 [in Top.UseAuto]
demo_tryfalse [in Top.UseTactics]
DeterministicImp.ceval_deterministic [in Top.UseAuto]
DeterministicImp.ceval_deterministic' [in Top.UseAuto]
DeterministicImp.ceval_deterministic'' [in Top.UseAuto]
DeterministicImp.ceval_deterministic''' [in Top.UseAuto]
DeterministicImp.ceval_deterministic'''' [in Top.UseAuto]
dist_exists_or [in Top.Logic]
dist_not_exists [in Top.Logic]
div_mod_dec_correct [in Top.Hoare2]
double_induction [in Top.Tactics]
double_injective [in Top.Tactics]
double_injective_FAILED [in Top.Tactics]
double_injective_take2 [in Top.Tactics]
double_injective_take2_FAILED [in Top.Tactics]
double_neg [in Top.Logic]
double_plus [in Top.Induction]
dpow2_down_correct [in Top.Hoare2]
duplicate_subst [in Top.Norm]
dup_lemma [in Top.LibTactics]
E
empty_is_empty [in Top.IndProp]EqualityExamples.demo_applys_eq_1 [in Top.UseTactics]
EqualityExamples.demo_applys_eq_2 [in Top.UseTactics]
EqualityExamples.demo_applys_eq_3 [in Top.UseTactics]
EqualityExamples.demo_fequals [in Top.UseTactics]
EqualityExamples.demo_substs [in Top.UseTactics]
EqualityExamples.mult_0_plus [in Top.UseTactics]
EqualityExamples.mult_0_plus' [in Top.UseTactics]
EqualityExamples.mult_0_plus'' [in Top.UseTactics]
equality_by_auto [in Top.UseAuto]
equates_0 [in Top.LibTactics]
equates_1 [in Top.LibTactics]
equates_2 [in Top.LibTactics]
equates_3 [in Top.LibTactics]
equates_4 [in Top.LibTactics]
equates_5 [in Top.LibTactics]
equates_6 [in Top.LibTactics]
evalF_eval [in Top.Smallstep]
eval_assign [in Top.PE]
eval__multistep [in Top.Smallstep]
evenb_double [in Top.Logic]
evenb_double_conv [in Top.Logic]
evenb_minus2 [in Top.IndProp]
evenb_S [in Top.Induction]
even5_nonsense [in Top.IndProp]
even_bool_prop [in Top.Logic]
evSS_ev [in Top.IndProp]
evSS_ev [in Top.IndProp]
ev'_ev [in Top.IndProp]
ev_double [in Top.IndProp]
ev_even [in Top.IndProp]
ev_even [in Top.IndProp]
ev_even_iff [in Top.IndProp]
ev_ev' [in Top.IndPrinciples]
ev_ev__ev [in Top.IndProp]
ev_minus2 [in Top.IndProp]
ev_minus2 [in Top.IndProp]
ev_minus2' [in Top.IndProp]
ev_plus4 [in Top.IndProp]
ev_plus4 [in Top.ProofObjects]
ev_plus_plus [in Top.IndProp]
ev_sum [in Top.IndProp]
ev_4 [in Top.IndProp]
ev_4 [in Top.ProofObjects]
ev_4' [in Top.IndProp]
ev_4' [in Top.ProofObjects]
ev_4'' [in Top.ProofObjects]
ev_8 [in Top.ProofObjects]
ExamplesInstantiations.substitution_preserves_typing [in Top.UseTactics]
ExamplesLets.demo_lets_underscore [in Top.UseTactics]
ExamplesLets.demo_lets_1 [in Top.UseTactics]
ExamplesLets.demo_lets_2 [in Top.UseTactics]
ExamplesLets.demo_lets_3 [in Top.UseTactics]
ExamplesLets.demo_lets_4 [in Top.UseTactics]
ExamplesLets.demo_lets_5 [in Top.UseTactics]
excluded_middle_irrefutable [in Top.Logic]
Exercises.curry_uncurry [in Top.Poly]
Exercises.fold_length_correct [in Top.Poly]
Exercises.uncurry_curry [in Top.Poly]
exists_example_2 [in Top.Logic]
ex_falso_quodlibet [in Top.Logic]
F
False_and_P_imp [in Top.HoareAsLogic]false_beq_id [in Top.Maps]
filter_exercise [in Top.Tactics]
filter_not_empty_In [in Top.IndProp]
filter_not_empty_In' [in Top.IndProp]
find_parity_correct [in Top.Hoare2]
find_parity_correct' [in Top.Hoare2]
fold_constants_aexp_sound [in Top.Equiv]
fold_constants_bexp_sound [in Top.Equiv]
fold_constants_com_sound [in Top.Equiv]
forallb_true_iff [in Top.Logic]
four_is_even [in Top.Logic]
free_in_context [in Top.Sub]
free_in_context [in Top.RecordSub]
free_in_context [in Top.Norm]
f_equal [in Top.Tactics]
G
GenExample.substitution_preserves_typing [in Top.UseTactics]H
has_type__wf [in Top.RecordSub]Himp.hoare_havoc [in Top.Hoare]
Himp.ptwice_cequiv_pcopy [in Top.Equiv]
Himp.pXY_cequiv_pYX [in Top.Equiv]
Himp.p1_may_diverge [in Top.Equiv]
Himp.p1_p2_equiv [in Top.Equiv]
Himp.p2_may_diverge [in Top.Equiv]
Himp.p3_p4_inequiv [in Top.Equiv]
Himp.p5_p6_equiv [in Top.Equiv]
Himp2.hoare_havoc_weakest [in Top.Hoare2]
hoare_asgn [in Top.Hoare]
hoare_asgn_fwd [in Top.Hoare]
hoare_asgn_fwd_exists [in Top.Hoare]
hoare_asgn_weakest [in Top.Hoare2]
hoare_consequence [in Top.Hoare]
hoare_consequence_post [in Top.Hoare]
hoare_consequence_pre [in Top.Hoare]
hoare_if [in Top.Hoare]
hoare_post_true [in Top.Hoare]
hoare_pre_false [in Top.Hoare]
hoare_proof_complete [in Top.HoareAsLogic]
hoare_proof_sound [in Top.HoareAsLogic]
hoare_seq [in Top.Hoare]
hoare_skip [in Top.Hoare]
hoare_while [in Top.Hoare]
H_Consequence_post [in Top.HoareAsLogic]
H_Consequence_pre [in Top.HoareAsLogic]
H_Post_True_deriv [in Top.HoareAsLogic]
H_Pre_False_deriv [in Top.HoareAsLogic]
I
identity_assignment [in Top.Equiv]identity_fn_applied_twice [in Top.Basics]
IFB_false [in Top.Equiv]
IFB_true [in Top.Equiv]
IFB_true_simple [in Top.Equiv]
iff_intro_swap [in Top.LibTactics]
iff_refl [in Top.Logic]
iff_reflect [in Top.IndProp]
iff_sym [in Top.Logic]
iff_trans [in Top.Equiv]
iff_trans [in Top.Logic]
If1.hoare_if1_good [in Top.Hoare]
if_minus_correct [in Top.Hoare2]
if_minus_plus [in Top.Hoare]
if_minus_plus_correct [in Top.Hoare2]
inbP [in Top.PE]
induct_height_max2 [in Top.LibTactics]
inequiv_exercise [in Top.Equiv]
instantiation_domains_match [in Top.Norm]
instantiation_drop [in Top.Norm]
instantiation_env_closed [in Top.Norm]
instantiation_R [in Top.Norm]
IntrovExamples.ceval_deterministic [in Top.UseTactics]
IntrovExamples.ceval_deterministic' [in Top.UseTactics]
IntrovExamples.dist_exists_or [in Top.UseTactics]
IntrovExamples.exists_impl [in Top.UseTactics]
inversion_ex1 [in Top.Tactics]
inversion_ex2 [in Top.Tactics]
inversion_ex4 [in Top.Tactics]
inversion_ex5 [in Top.Tactics]
InvertsExamples.ceval_deterministic [in Top.UseTactics]
InvertsExamples.ceval_deterministic' [in Top.UseTactics]
InvertsExamples.skip_left [in Top.UseTactics]
InvertsExamples.skip_left' [in Top.UseTactics]
in_app_iff [in Top.Logic]
In_map [in Top.Logic]
In_map_iff [in Top.Logic]
in_re_match [in Top.IndProp]
in_split [in Top.IndProp]
is_wp_example [in Top.Hoare2]
L
leb_complete [in Top.IndProp]leb_correct [in Top.IndProp]
leb_iff [in Top.IndProp]
leb_refl [in Top.Induction]
leb_true_trans [in Top.IndProp]
LeModule.test_le1 [in Top.IndProp]
LeModule.test_le2 [in Top.IndProp]
LeModule.test_le3 [in Top.IndProp]
le_antisym [in Top.Auto]
le_antisymmetric [in Top.Rel]
le_not_a_partial_function [in Top.Rel]
le_not_symmetric [in Top.Rel]
le_order [in Top.Rel]
le_plus_l [in Top.IndProp]
le_reflexive [in Top.Rel]
le_Sn_le [in Top.Rel]
le_Sn_n [in Top.Rel]
le_step [in Top.Rel]
le_S_n [in Top.Rel]
le_trans [in Top.IndProp]
le_trans [in Top.Rel]
lookup_field_in_value [in Top.RecordSub]
Loop.ceval_count_complete [in Top.PE]
Loop.ceval_count_sound [in Top.PE]
Loop.pe_ceval_count_le [in Top.PE]
Loop.pe_compare_nil_lookup [in Top.PE]
Loop.pe_compare_nil_update [in Top.PE]
Loop.pe_com_complete [in Top.PE]
Loop.pe_com_correct [in Top.PE]
Loop.pe_com_sound [in Top.PE]
loop_never_stops [in Top.Imp]
loop_unrolling [in Top.Equiv]
ltac_database_provide [in Top.LibTactics]
ltac_something_eq [in Top.LibTactics]
ltac_something_hide [in Top.LibTactics]
ltac_something_show [in Top.LibTactics]
lt_S [in Top.IndProp]
lt_trans [in Top.Rel]
lt_trans' [in Top.Rel]
lt_trans'' [in Top.Rel]
l1 [in Top.Hoare2]
l2 [in Top.Hoare2]
l3 [in Top.Hoare2]
l3' [in Top.Hoare2]
l4 [in Top.Hoare2]
M
map_rev [in Top.Poly]minus_diag [in Top.Induction]
MStar' [in Top.IndProp]
MStar'' [in Top.IndProp]
MStar1 [in Top.IndProp]
msubst_abs [in Top.Norm]
msubst_app [in Top.Norm]
msubst_closed [in Top.Norm]
msubst_preserves_typing [in Top.Norm]
msubst_R [in Top.Norm]
msubst_var [in Top.Norm]
multistep_App2 [in Top.Norm]
multistep_congr_1 [in Top.Smallstep]
multistep_congr_2 [in Top.Smallstep]
multistep_preserves_R [in Top.Norm]
multistep_preserves_R' [in Top.Norm]
multistep__eval [in Top.Smallstep]
multi_R [in Top.Smallstep]
multi_trans [in Top.Smallstep]
mult_assoc [in Top.Induction]
mult_comm [in Top.Induction]
mult_eq_0 [in Top.Logic]
mult_plus_distr_r [in Top.Induction]
mult_S_1 [in Top.Basics]
mult_0 [in Top.Logic]
mult_0_l [in Top.Basics]
mult_0_plus [in Top.Basics]
mult_0_plus' [in Top.Induction]
mult_0_r [in Top.Induction]
mult_0_r' [in Top.IndPrinciples]
mult_0_r'' [in Top.IndPrinciples]
mult_0_3 [in Top.Logic]
mult_1_l [in Top.Induction]
MUnion' [in Top.IndProp]
mupdate_drop [in Top.Norm]
mupdate_lookup [in Top.Norm]
MyEquality.four [in Top.ProofObjects]
MyEquality.leibniz_equality [in Top.ProofObjects]
N
NaryExamples.demo_branch [in Top.UseTactics]NaryExamples.demo_splits [in Top.UseTactics]
NaryExamples.progress [in Top.UseTactics]
NatList.app_assoc [in Top.Lists]
NatList.app_assoc4 [in Top.Lists]
NatList.app_length [in Top.Lists]
NatList.app_nil_r [in Top.Lists]
NatList.bag_theorem [in Top.Lists]
NatList.beq_natlist_refl [in Top.Lists]
NatList.ble_n_Sn [in Top.Lists]
NatList.count_member_nonzero [in Top.Lists]
NatList.fst_swap_is_snd [in Top.Lists]
NatList.nil_app [in Top.Lists]
NatList.nonzeros_app [in Top.Lists]
NatList.option_elim_hd [in Top.Lists]
NatList.remove_decreases_count [in Top.Lists]
NatList.rev_involutive [in Top.Lists]
NatList.rev_length [in Top.Lists]
NatList.rev_length_firsttry [in Top.Lists]
NatList.snd_fst_is_swap [in Top.Lists]
NatList.surjective_pairing [in Top.Lists]
NatList.surjective_pairing' [in Top.Lists]
NatList.surjective_pairing_stuck [in Top.Lists]
NatList.tl_length_pred [in Top.Lists]
nat_canonical [in Top.Types]
negation_study_1 [in Top.UseAuto]
negation_study_2 [in Top.UseAuto]
negb_involutive [in Top.Basics]
next_nat_closure_is_le [in Top.Rel]
next_nat_partial_function [in Top.Rel]
nf_is_value [in Top.Smallstep]
nf_same_as_value [in Top.Smallstep]
normalization [in Top.Norm]
normalize_ex [in Top.Types]
normalize_ex' [in Top.Types]
normal_forms_unique [in Top.Smallstep]
not_both_true_and_false [in Top.Logic]
not_exists_dist [in Top.Logic]
not_False [in Top.Logic]
not_implies_our_not [in Top.Logic]
not_true_iff_false [in Top.Logic]
not_true_is_false [in Top.Logic]
not_true_is_false' [in Top.Logic]
no_whiles_eqv [in Top.Imp]
nth_error_after_last [in Top.Tactics]
n_le_m__Sn_le_Sm [in Top.IndProp]
O
omega_demo_1 [in Top.UseAuto]omega_demo_2 [in Top.UseAuto]
omega_demo_3 [in Top.UseAuto]
omega_demo_4 [in Top.UseAuto]
one_not_even [in Top.IndProp]
orb_true_iff [in Top.Logic]
order_matters_1 [in Top.UseAuto]
order_matters_2 [in Top.UseAuto]
or_assoc [in Top.Logic]
or_commut [in Top.Logic]
or_distributes_over_and [in Top.Logic]
or_example [in Top.Logic]
or_intro [in Top.Logic]
O_le_n [in Top.IndProp]
P
parity_correct [in Top.Hoare2]parity_dec_correct [in Top.Hoare2]
parity_ge_2 [in Top.Hoare2]
parity_lt_2 [in Top.Hoare2]
PartialMap.update_eq [in Top.Lists]
PartialMap.update_neq [in Top.Lists]
pe_add_correct [in Top.PE]
pe_aexp_correct [in Top.PE]
pe_aexp_correct_weak [in Top.PE]
pe_bexp_correct [in Top.PE]
pe_block_correct [in Top.PE]
pe_compare_correct [in Top.PE]
pe_compare_removes [in Top.PE]
pe_compare_update [in Top.PE]
pe_com_complete [in Top.PE]
pe_com_correct [in Top.PE]
pe_com_sound [in Top.PE]
pe_consistent_update [in Top.PE]
pe_disagree_domain [in Top.PE]
pe_domain [in Top.PE]
pe_program_correct [in Top.PE]
pe_removes_correct [in Top.PE]
pe_remove_correct [in Top.PE]
pe_unique_correct [in Top.PE]
pe_update_consistent [in Top.PE]
pe_update_correct [in Top.PE]
pe_update_update_add [in Top.PE]
pe_update_update_remove [in Top.PE]
pigeonhole_principle [in Top.IndProp]
plus2_spec [in Top.Imp]
plus_assoc [in Top.Induction]
plus_assoc' [in Top.Induction]
plus_assoc' [in Top.IndPrinciples]
plus_assoc'' [in Top.Induction]
plus_ble_compat_l [in Top.Induction]
plus_comm [in Top.Induction]
plus_comm' [in Top.IndPrinciples]
plus_comm'' [in Top.IndPrinciples]
plus_comm3 [in Top.Logic]
plus_comm3_take2 [in Top.Logic]
plus_comm_ext [in Top.Logic]
plus_fact_is_true [in Top.Logic]
plus_id_example [in Top.Basics]
plus_id_exercise [in Top.Basics]
plus_lt [in Top.IndProp]
plus_n_n_injective [in Top.Tactics]
plus_n_O [in Top.Basics]
plus_n_O [in Top.Induction]
plus_n_O_firsttry [in Top.Induction]
plus_n_O_secondtry [in Top.Induction]
plus_n_Sm [in Top.Induction]
plus_one_r' [in Top.IndPrinciples]
plus_O_n [in Top.Basics]
plus_O_n' [in Top.Basics]
plus_rearrange [in Top.Induction]
plus_rearrange_firsttry [in Top.Induction]
plus_swap [in Top.Induction]
plus_swap' [in Top.Induction]
plus_1_l [in Top.Basics]
plus_1_neq_0 [in Top.Basics]
plus_1_neq_0' [in Top.Basics]
plus_1_neq_0_firsttry [in Top.Basics]
plus_2_2_is_4 [in Top.Logic]
pow2_le_1 [in Top.Hoare2]
pow2_plus_1 [in Top.Hoare2]
preservation [in Top.Norm]
preservation [in Top.RecordSub]
preservation [in Top.Types]
preservation [in Top.Sub]
PreservationProgressReferences.nth_eq_last' [in Top.UseAuto]
PreservationProgressReferences.preservation [in Top.UseAuto]
PreservationProgressReferences.preservation' [in Top.UseAuto]
PreservationProgressReferences.preservation_ref [in Top.UseAuto]
PreservationProgressReferences.progress [in Top.UseAuto]
PreservationProgressStlc.preservation [in Top.UseAuto]
PreservationProgressStlc.preservation' [in Top.UseAuto]
PreservationProgressStlc.progress [in Top.UseAuto]
PreservationProgressStlc.progress' [in Top.UseAuto]
preservation' [in Top.Types]
progress [in Top.RecordSub]
progress [in Top.Sub]
progress [in Top.Types]
proj1 [in Top.Logic]
proj2 [in Top.Logic]
Props.and_comm [in Top.ProofObjects]
Pumping.napp_plus [in Top.IndProp]
Pumping.pumping [in Top.IndProp]
pup_to_2_ceval [in Top.Imp]
R
rcd_types_match [in Top.RecordSub]reduce_to_zero_correct' [in Top.Hoare2]
reflect_iff [in Top.IndProp]
refl_aequiv [in Top.Equiv]
refl_bequiv [in Top.Equiv]
refl_cequiv [in Top.Equiv]
reg_exp_of_list_spec [in Top.IndProp]
RepeatExercise.ex1_repeat_works [in Top.Hoare]
Repeat.ceval_deterministic [in Top.Auto]
Repeat.ceval_deterministic' [in Top.Auto]
restricted_excluded_middle [in Top.Logic]
rev_app_distr [in Top.Poly]
rev_exercise1 [in Top.Tactics]
rev_involutive [in Top.Poly]
re_not_empty_correct [in Top.IndProp]
RingDemo.ring_demo [in Top.UseAuto]
rsc_R [in Top.Rel]
rsc_trans [in Top.Rel]
rtc_rsc_coincide [in Top.Rel]
R.R_equiv_fR [in Top.IndProp]
R_halts [in Top.Norm]
R_typable_empty [in Top.Norm]
S
search_depth_0 [in Top.UseAuto]search_depth_1 [in Top.UseAuto]
search_depth_3 [in Top.UseAuto]
search_depth_4 [in Top.UseAuto]
search_depth_5 [in Top.UseAuto]
Semantics.multistep_eval_ind [in Top.UseAuto]
Semantics.multistep__eval [in Top.UseAuto]
Semantics.multistep__eval' [in Top.UseAuto]
Semantics.multistep__eval'' [in Top.UseAuto]
seq_assoc [in Top.Equiv]
sillyfun1_odd [in Top.Tactics]
sillyfun1_odd_FAILED [in Top.Tactics]
sillyfun_false [in Top.Tactics]
silly1 [in Top.Tactics]
silly1 [in Top.Hoare]
silly2 [in Top.Tactics]
silly2 [in Top.Hoare]
silly2a [in Top.Tactics]
silly2_eassumption [in Top.Hoare]
silly2_fixed [in Top.Hoare]
silly3 [in Top.Tactics]
silly3' [in Top.Tactics]
silly3_firsttry [in Top.Tactics]
silly_ex [in Top.Tactics]
silly_fact_1 [in Top.Tactics]
silly_fact_2 [in Top.Tactics]
silly_fact_2' [in Top.Tactics]
silly_fact_2_FAILED [in Top.Tactics]
SimpleArith2.step_deterministic [in Top.Smallstep]
SimpleArith2.step_deterministic_alt [in Top.Smallstep]
SkipExample.ceval_deterministic [in Top.UseTactics]
SkipExample.demo_skipH [in Top.UseTactics]
SkipExample.mult_0_plus [in Top.UseTactics]
skip_left [in Top.Equiv]
skip_right [in Top.Equiv]
slow_assignment_dec_correct [in Top.Hoare2]
Sn_le_Sm__n_le_m [in Top.IndProp]
solved_by_jauto [in Top.UseAuto]
solving_by_apply [in Top.UseAuto]
solving_by_eapply [in Top.UseAuto]
solving_by_reflexivity [in Top.UseAuto]
solving_conj_goal [in Top.UseAuto]
solving_conj_hyp [in Top.UseAuto]
solving_conj_hyp' [in Top.UseAuto]
solving_conj_hyp_forall [in Top.UseAuto]
solving_conj_more [in Top.UseAuto]
solving_disj_goal [in Top.UseAuto]
solving_disj_hyp [in Top.UseAuto]
solving_exists_goal [in Top.UseAuto]
solving_exists_hyp [in Top.UseAuto]
solving_tauto [in Top.UseAuto]
SortExamples.ceval_deterministic [in Top.UseTactics]
soundness [in Top.Types]
split_combine [in Top.Tactics]
sqrt_correct [in Top.Hoare2]
square_dec'_correct [in Top.Hoare2]
square_dec_correct [in Top.Hoare2]
square_mult [in Top.Tactics]
square_simpler_dec_correct [in Top.Hoare2]
SSSSev__even [in Top.IndProp]
stack_step_deterministic [in Top.Smallstep]
star_app [in Top.IndProp]
star_app [in Top.IndProp]
star_app [in Top.IndProp]
step_deterministic [in Top.Types]
step_deterministic [in Top.Norm]
step_deterministic [in Top.Smallstep]
step_normalizing [in Top.Smallstep]
step_preserves_halting [in Top.Norm]
step_preserves_R [in Top.Norm]
step_preserves_record_tm [in Top.RecordSub]
step_preserves_R' [in Top.Norm]
step__eval [in Top.Smallstep]
STLCChecker.beq_ty_refl [in Top.Typechecking]
STLCChecker.beq_ty__eq [in Top.Typechecking]
STLCChecker.type_checking_complete [in Top.Typechecking]
STLCChecker.type_checking_sound [in Top.Typechecking]
STLCExtendedRecords.context_invariance [in Top.Records]
STLCExtendedRecords.free_in_context [in Top.Records]
STLCExtendedRecords.has_type__wf [in Top.Records]
STLCExtendedRecords.lookup_field_in_value [in Top.Records]
STLCExtendedRecords.preservation [in Top.Records]
STLCExtendedRecords.progress [in Top.Records]
STLCExtendedRecords.step_preserves_record_tm [in Top.Records]
STLCExtendedRecords.substitution_preserves_typing [in Top.Records]
STLCExtendedRecords.typing_example_2 [in Top.Records]
STLCExtendedRecords.wf_rcd_lookup [in Top.Records]
STLCExtended.context_invariance [in Top.MoreStlc]
STLCExtended.free_in_context [in Top.MoreStlc]
STLCExtended.preservation [in Top.MoreStlc]
STLCExtended.progress [in Top.MoreStlc]
STLCExtended.substitution_preserves_typing [in Top.MoreStlc]
STLCProp.canonical_forms_bool [in Top.StlcProp]
STLCProp.canonical_forms_fun [in Top.StlcProp]
STLCProp.context_invariance [in Top.StlcProp]
STLCProp.free_in_context [in Top.StlcProp]
STLCProp.preservation [in Top.StlcProp]
STLCProp.progress [in Top.StlcProp]
STLCProp.progress' [in Top.StlcProp]
STLCProp.soundness [in Top.StlcProp]
STLCProp.substitution_preserves_typing [in Top.StlcProp]
STLCProp.typable_empty__closed [in Top.StlcProp]
STLCRef.assign_pres_store_typing [in Top.References]
STLCRef.context_invariance [in Top.References]
STLCRef.extends_app [in Top.References]
STLCRef.extends_lookup [in Top.References]
STLCRef.extends_refl [in Top.References]
STLCRef.free_in_context [in Top.References]
STLCRef.length_extends [in Top.References]
STLCRef.length_replace [in Top.References]
STLCRef.lookup_replace_eq [in Top.References]
STLCRef.lookup_replace_neq [in Top.References]
STLCRef.nth_eq_last [in Top.References]
STLCRef.preservation [in Top.References]
STLCRef.preservation_wrong1 [in Top.References]
STLCRef.preservation_wrong2 [in Top.References]
STLCRef.progress [in Top.References]
STLCRef.RefsAndNontermination.factorial_type [in Top.References]
STLCRef.RefsAndNontermination.loop_fun_step_self [in Top.References]
STLCRef.RefsAndNontermination.loop_steps_to_loop_fun [in Top.References]
STLCRef.RefsAndNontermination.loop_typeable [in Top.References]
STLCRef.replace_nil [in Top.References]
STLCRef.store_weakening [in Top.References]
STLCRef.store_well_typed_app [in Top.References]
STLCRef.substitution_preserves_typing [in Top.References]
STLC.step_example1 [in Top.Stlc]
STLC.step_example1' [in Top.Stlc]
STLC.step_example2 [in Top.Stlc]
STLC.step_example2' [in Top.Stlc]
STLC.step_example3 [in Top.Stlc]
STLC.step_example3' [in Top.Stlc]
STLC.step_example4 [in Top.Stlc]
STLC.step_example4' [in Top.Stlc]
STLC.step_example5 [in Top.Stlc]
STLC.step_example5_with_normalize [in Top.Stlc]
STLC.substi_correct [in Top.Stlc]
strong_progress [in Top.Smallstep]
substitution_preserves_typing [in Top.RecordSub]
substitution_preserves_typing [in Top.Sub]
substitution_preserves_typing [in Top.Norm]
subst_closed [in Top.Norm]
subst_inequiv [in Top.Equiv]
subst_msubst [in Top.Norm]
subst_not_afi [in Top.Norm]
subtract_slowly_dec_correct [in Top.Hoare2]
subtype__wf [in Top.RecordSub]
SubtypingInversion.abs_arrow [in Top.UseAuto]
SubtypingInversion.abs_arrow' [in Top.UseAuto]
SubtypingInversion.substitution_preserves_typing [in Top.UseAuto]
sub_inversion_arrow [in Top.RecordSub]
sub_inversion_arrow [in Top.Sub]
sub_inversion_Bool [in Top.Sub]
succ_inj [in Top.Logic]
swap_correct [in Top.Hoare2]
swap_exercise [in Top.Hoare]
swap_if_branches [in Top.Equiv]
swap_noninterfering_assignments [in Top.Equiv]
swap_subst [in Top.Norm]
sym_aequiv [in Top.Equiv]
sym_bequiv [in Top.Equiv]
sym_cequiv [in Top.Equiv]
s_compile_correct [in Top.Imp]
S_inj [in Top.Tactics]
S_injective [in Top.Tactics]
S_nbeq_0 [in Top.Induction]
T
Temp1.value_not_same_as_normal_form [in Top.Smallstep]Temp2.value_not_same_as_normal_form [in Top.Smallstep]
Temp3.value_not_same_as_normal_form [in Top.Smallstep]
Temp4.step_deterministic [in Top.Smallstep]
Temp4.strong_progress [in Top.Smallstep]
test_multistep_1 [in Top.Smallstep]
test_multistep_1' [in Top.Smallstep]
test_multistep_2 [in Top.Smallstep]
test_multistep_3 [in Top.Smallstep]
test_multistep_4 [in Top.Smallstep]
transitivity_bad_hint_1 [in Top.UseAuto]
transitivity_workaround_1 [in Top.UseAuto]
transitivity_workaround_2 [in Top.UseAuto]
trans_aequiv [in Top.Equiv]
trans_bequiv [in Top.Equiv]
trans_cequiv [in Top.Equiv]
trans_eq [in Top.Tactics]
True_is_true [in Top.Logic]
tr_rev_correct [in Top.Logic]
two_loops_correct [in Top.Hoare2]
typable_empty__closed [in Top.Norm]
typing_inversion_abs [in Top.RecordSub]
typing_inversion_abs [in Top.Sub]
typing_inversion_app [in Top.RecordSub]
typing_inversion_app [in Top.Sub]
typing_inversion_false [in Top.Sub]
typing_inversion_if [in Top.Sub]
typing_inversion_proj [in Top.RecordSub]
typing_inversion_rcons [in Top.RecordSub]
typing_inversion_true [in Top.Sub]
typing_inversion_unit [in Top.Sub]
typing_inversion_var [in Top.Sub]
typing_inversion_var [in Top.RecordSub]
t_update_eq [in Top.Maps]
t_update_neq [in Top.Maps]
t_update_permute [in Top.Maps]
t_update_same [in Top.Maps]
t_update_shadow [in Top.Maps]
U
UnfoldsExample.bexp_eval_true [in Top.UseTactics]update_eq [in Top.Maps]
update_neq [in Top.Maps]
update_permute [in Top.Maps]
update_same [in Top.Maps]
update_shadow [in Top.Maps]
V
vacuous_substitution [in Top.Norm]value_halts [in Top.Norm]
value_is_nf [in Top.Types]
value_is_nf [in Top.Smallstep]
value__normal [in Top.Norm]
verification_correct [in Top.Hoare2]
W
wf_rcd_lookup [in Top.RecordSub]WHILE_false [in Top.Equiv]
WHILE_true [in Top.Equiv]
WHILE_true_nonterm [in Top.Equiv]
working_of_auto_1 [in Top.UseAuto]
working_of_auto_2 [in Top.UseAuto]
wp_is_precondition [in Top.HoareAsLogic]
wp_is_weakest [in Top.HoareAsLogic]
Z
zero_nbeq_plus_1 [in Top.Basics]zero_nbeq_S [in Top.Induction]
zero_not_one [in Top.Logic]
zero_not_one' [in Top.Logic]
zero_or_succ [in Top.Logic]
zprop_preserving [in Top.Equiv]
Axiom Index
E
EqualityExamples.big_expression_using [in Top.UseTactics]ExamplesLets.typing_inversion_var [in Top.UseTactics]
F
functional_extensionality [in Top.Logic]G
gt_not_le [in Top.UseAuto]I
inj_pair2 [in Top.LibTactics]L
le_gt_false [in Top.UseAuto]le_not_gt [in Top.UseAuto]
P
P [in Top.UseAuto]S
subtype [in Top.UseAuto]subtype_refl [in Top.UseAuto]
subtype_trans [in Top.UseAuto]
T
typ [in Top.UseAuto]Inductive Index
A
aevalR_division.aevalR [in Top.Imp]aevalR_division.aexp [in Top.Imp]
aevalR_extended.aevalR [in Top.Imp]
aevalR_extended.aexp [in Top.Imp]
aexp [in Top.Imp]
AExp.aevalR [in Top.Imp]
AExp.aevalR_first_try.aevalR [in Top.Imp]
AExp.aexp [in Top.Imp]
AExp.bexp [in Top.Imp]
appears_free_in [in Top.Norm]
appears_free_in [in Top.Sub]
appears_free_in [in Top.RecordSub]
astep [in Top.Smallstep]
aval [in Top.Smallstep]
B
baz [in Top.Lists]bexp [in Top.Imp]
block [in Top.PE]
bool [in Top.Basics]
boollist [in Top.Poly]
Boxer [in Top.LibTactics]
BreakImp.ceval [in Top.Imp]
BreakImp.com [in Top.Imp]
BreakImp.status [in Top.Imp]
bstep [in Top.Smallstep]
bvalue [in Top.Types]
byntree [in Top.IndPrinciples]
C
ceval [in Top.Imp]chartype [in Top.ImpParser]
CImp.com [in Top.Smallstep]
CImp.cstep [in Top.Smallstep]
clos_refl_trans [in Top.Rel]
clos_refl_trans_1n [in Top.Rel]
com [in Top.Imp]
Combined.step [in Top.Smallstep]
Combined.tm [in Top.Smallstep]
Combined.value [in Top.Smallstep]
cstep [in Top.Smallstep]
D
day [in Top.Basics]dcom [in Top.Hoare2]
E
ev [in Top.IndProp]ev [in Top.Hoare2]
eval [in Top.Smallstep]
ev' [in Top.IndProp]
exp_match [in Top.IndProp]
ExSet [in Top.IndPrinciples]
F
foo' [in Top.IndPrinciples]H
has_type [in Top.Sub]has_type [in Top.Types]
has_type [in Top.Norm]
has_type [in Top.RecordSub]
Himp.ceval [in Top.Hoare]
Himp.ceval [in Top.Equiv]
Himp.com [in Top.Hoare]
Himp.com [in Top.Equiv]
hoare_proof [in Top.HoareAsLogic]
I
id [in Top.Lists]id [in Top.Maps]
If1.ceval [in Top.Hoare]
If1.com [in Top.Hoare]
instantiation [in Top.Norm]
L
le [in Top.IndPrinciples]LeModule.le [in Top.IndProp]
list [in Top.Poly]
list' [in Top.Poly]
Loop.ceval_count [in Top.PE]
Loop.pe_ceval_count [in Top.PE]
Loop.pe_com [in Top.PE]
Ltac_database_token [in Top.LibTactics]
ltac_Mark [in Top.LibTactics]
ltac_No_arg [in Top.LibTactics]
ltac_Wild [in Top.LibTactics]
ltac_Wilds [in Top.LibTactics]
M
multi [in Top.Smallstep]MumbleGrumble.grumble [in Top.Poly]
MumbleGrumble.mumble [in Top.Poly]
MyEquality.eq [in Top.ProofObjects]
N
natlist [in Top.IndPrinciples]NatList.natlist [in Top.Lists]
NatList.natoption [in Top.Lists]
NatList.natprod [in Top.Lists]
natlist1 [in Top.IndPrinciples]
next_even [in Top.IndProp]
next_nat [in Top.IndProp]
nostutter [in Top.IndProp]
no_whilesR [in Top.Imp]
nvalue [in Top.Types]
O
option [in Top.Poly]optionE [in Top.ImpParser]
P
parity_label [in Top.PE]PartialMap.partial_map [in Top.Lists]
peval [in Top.PE]
pe_ceval [in Top.PE]
pe_com [in Top.PE]
pe_peval [in Top.PE]
Playground1.nat [in Top.Basics]
prod [in Top.Poly]
Props.And.and [in Top.ProofObjects]
Props.Ex.ex [in Top.ProofObjects]
Props.False [in Top.ProofObjects]
Props.Or.or [in Top.ProofObjects]
Props.True [in Top.ProofObjects]
R
record_tm [in Top.RecordSub]record_ty [in Top.RecordSub]
reflect [in Top.IndProp]
reg_exp [in Top.IndProp]
RepeatExercise.ceval [in Top.Hoare]
RepeatExercise.com [in Top.Hoare]
repeats [in Top.IndProp]
Repeat.ceval [in Top.Auto]
Repeat.com [in Top.Auto]
rgb [in Top.IndPrinciples]
R.R [in Top.IndProp]
S
SimpleArith1.step [in Top.Smallstep]sinstr [in Top.Imp]
square_of [in Top.IndProp]
stack_step [in Top.Smallstep]
step [in Top.Smallstep]
step [in Top.Types]
step [in Top.RecordSub]
step [in Top.Sub]
step [in Top.Norm]
STLCArith.tm [in Top.StlcProp]
STLCArith.ty [in Top.StlcProp]
STLCExtendedRecords.appears_free_in [in Top.Records]
STLCExtendedRecords.FirstTry.ty [in Top.Records]
STLCExtendedRecords.has_type [in Top.Records]
STLCExtendedRecords.record_tm [in Top.Records]
STLCExtendedRecords.record_ty [in Top.Records]
STLCExtendedRecords.step [in Top.Records]
STLCExtendedRecords.tm [in Top.Records]
STLCExtendedRecords.ty [in Top.Records]
STLCExtendedRecords.value [in Top.Records]
STLCExtendedRecords.well_formed_ty [in Top.Records]
STLCExtended.appears_free_in [in Top.MoreStlc]
STLCExtended.has_type [in Top.MoreStlc]
STLCExtended.step [in Top.MoreStlc]
STLCExtended.tm [in Top.MoreStlc]
STLCExtended.ty [in Top.MoreStlc]
STLCExtended.value [in Top.MoreStlc]
STLCProp.appears_free_in [in Top.StlcProp]
STLCRef.appears_free_in [in Top.References]
STLCRef.extends [in Top.References]
STLCRef.has_type [in Top.References]
STLCRef.RefsAndNontermination.step_closure [in Top.References]
STLCRef.step [in Top.References]
STLCRef.tm [in Top.References]
STLCRef.ty [in Top.References]
STLCRef.value [in Top.References]
STLC.has_type [in Top.Stlc]
STLC.step [in Top.Stlc]
STLC.substi [in Top.Stlc]
STLC.tm [in Top.Stlc]
STLC.ty [in Top.Stlc]
STLC.value [in Top.Stlc]
subtype [in Top.Sub]
subtype [in Top.RecordSub]
T
Temp1.step [in Top.Smallstep]Temp1.value [in Top.Smallstep]
Temp2.step [in Top.Smallstep]
Temp2.value [in Top.Smallstep]
Temp3.step [in Top.Smallstep]
Temp3.value [in Top.Smallstep]
Temp4.step [in Top.Smallstep]
Temp4.Temp5.step [in Top.Smallstep]
Temp4.tm [in Top.Smallstep]
Temp4.value [in Top.Smallstep]
tm [in Top.RecordSub]
tm [in Top.Types]
tm [in Top.Smallstep]
tm [in Top.Sub]
tm [in Top.Norm]
tree [in Top.IndPrinciples]
ty [in Top.RecordSub]
ty [in Top.Sub]
ty [in Top.Types]
ty [in Top.Norm]
V
value [in Top.RecordSub]value [in Top.Norm]
value [in Top.Smallstep]
value [in Top.Sub]
var_not_used_in_aexp [in Top.Equiv]
W
well_formed_ty [in Top.RecordSub]wrong_ev [in Top.IndProp]
Y
yesno [in Top.IndPrinciples]Section Index
D
DemoAbsurd1 [in Top.UseAuto]E
equatesLemma [in Top.LibTactics]H
HintsTransitivity [in Top.UseAuto]Abbreviation Index
E
Examples.A [in Top.RecordSub]Examples.A [in Top.Sub]
Examples.B [in Top.RecordSub]
Examples.B [in Top.Sub]
Examples.C [in Top.Sub]
Examples.C [in Top.RecordSub]
Examples.Float [in Top.Sub]
Examples.i [in Top.RecordSub]
Examples.Integer [in Top.Sub]
Examples.j [in Top.RecordSub]
Examples.k [in Top.RecordSub]
Examples.String [in Top.Sub]
Examples.x [in Top.RecordSub]
Examples.x [in Top.Sub]
Examples.y [in Top.Sub]
Examples.y [in Top.RecordSub]
Examples.z [in Top.RecordSub]
Examples.z [in Top.Sub]
M
multistep [in Top.Norm]S
step_normal_form [in Top.Types]step_normal_form [in Top.Norm]
STLCExtendedRecords.a [in Top.Records]
STLCExtendedRecords.A [in Top.Records]
STLCExtendedRecords.B [in Top.Records]
STLCExtendedRecords.f [in Top.Records]
STLCExtendedRecords.g [in Top.Records]
STLCExtendedRecords.i1 [in Top.Records]
STLCExtendedRecords.i2 [in Top.Records]
STLCExtendedRecords.k [in Top.Records]
STLCExtendedRecords.l [in Top.Records]
STLCExtendedRecords.multistep [in Top.Records]
STLCExtended.Examples.a [in Top.MoreStlc]
STLCExtended.Examples.eo [in Top.MoreStlc]
STLCExtended.Examples.eq [in Top.MoreStlc]
STLCExtended.Examples.even [in Top.MoreStlc]
STLCExtended.Examples.evenodd [in Top.MoreStlc]
STLCExtended.Examples.f [in Top.MoreStlc]
STLCExtended.Examples.g [in Top.MoreStlc]
STLCExtended.Examples.i1 [in Top.MoreStlc]
STLCExtended.Examples.i2 [in Top.MoreStlc]
STLCExtended.Examples.k [in Top.MoreStlc]
STLCExtended.Examples.l [in Top.MoreStlc]
STLCExtended.Examples.m [in Top.MoreStlc]
STLCExtended.Examples.n [in Top.MoreStlc]
STLCExtended.Examples.odd [in Top.MoreStlc]
STLCExtended.Examples.processSum [in Top.MoreStlc]
STLCExtended.Examples.x [in Top.MoreStlc]
STLCExtended.Examples.y [in Top.MoreStlc]
STLCExtended.multistep [in Top.MoreStlc]
STLC.idB [in Top.Stlc]
STLC.idBB [in Top.Stlc]
STLC.idBBBB [in Top.Stlc]
STLC.k [in Top.Stlc]
STLC.multistep [in Top.Stlc]
STLC.notB [in Top.Stlc]
Definition Index
A
add1 [in Top.ProofObjects]admit [in Top.SfLib]
admit [in Top.Basics]
aequiv [in Top.Equiv]
aeval [in Top.Imp]
AExp.aeval [in Top.Imp]
AExp.beval [in Top.Imp]
AExp.optimize_0plus [in Top.Imp]
AExp.optimize_0plus_b [in Top.Imp]
AExp.silly_presburger_example [in Top.Imp]
AExp.test_aeval1 [in Top.Imp]
AExp.test_optimize_0plus [in Top.Imp]
aexp1 [in Top.Imp]
All [in Top.Logic]
andb [in Top.Basics]
andb3 [in Top.Basics]
and_example [in Top.Logic]
and_example' [in Top.Logic]
and_exercise [in Top.Logic]
antisymmetric [in Top.Rel]
app [in Top.Poly]
Assertion [in Top.Hoare]
assert_implies [in Top.Hoare]
assign [in Top.PE]
assigned [in Top.PE]
assn_sub [in Top.Hoare]
assn_sub_example [in Top.Hoare]
astep_example1 [in Top.Types]
astep_example1' [in Top.Types]
astep_example1'' [in Top.Types]
astep_example1''' [in Top.Types]
atrans_sound [in Top.Equiv]
auto_example_1 [in Top.Auto]
auto_example_1' [in Top.Auto]
auto_example_2 [in Top.Auto]
auto_example_3 [in Top.Auto]
auto_example_4 [in Top.Auto]
auto_example_5 [in Top.Auto]
auto_example_6 [in Top.Auto]
auto_example_6' [in Top.Auto]
auto_example_7 [in Top.Auto]
auto_example_7' [in Top.Auto]
auto_example_8 [in Top.Auto]
auto_example_8' [in Top.Auto]
B
bar [in Top.Tactics]bassn [in Top.Hoare]
bequiv [in Top.Equiv]
beq_id [in Top.Maps]
beq_id [in Top.Lists]
beq_list [in Top.Logic]
beq_nat [in Top.Basics]
beval [in Top.Imp]
bexp1 [in Top.Imp]
bignumber [in Top.ImpParser]
blt_nat [in Top.Basics]
btrans_sound [in Top.Equiv]
build_symtable [in Top.ImpParser]
C
capprox [in Top.Equiv]cequiv [in Top.Equiv]
ceval_example1 [in Top.Imp]
ceval_example2 [in Top.Imp]
ceval_fun_no_while [in Top.Imp]
ceval_step [in Top.ImpCEvalFun]
ceval_step1 [in Top.ImpCEvalFun]
ceval_step2 [in Top.ImpCEvalFun]
ceval_step3 [in Top.ImpCEvalFun]
CImp.cmultistep [in Top.Smallstep]
CImp.par_loop [in Top.Smallstep]
CImp.par_loop_example_0 [in Top.Smallstep]
CImp.par_loop_example_2 [in Top.Smallstep]
classifyChar [in Top.ImpParser]
closed [in Top.Norm]
closed_env [in Top.Norm]
cmin [in Top.Equiv]
COIND [in Top.LibTactics]
combine [in Top.Poly]
combine_odd_even [in Top.Logic]
compiler_is_correct_statement [in Top.Smallstep]
congruence_example [in Top.Equiv]
constfun [in Top.Poly]
constfun_example1 [in Top.Poly]
constfun_example2 [in Top.Poly]
context [in Top.Norm]
context [in Top.RecordSub]
context [in Top.Sub]
countoddmembers' [in Top.Poly]
ctrans_sound [in Top.Equiv]
c3 [in Top.Equiv]
c4 [in Top.Equiv]
D
dec_correct [in Top.Hoare2]dec_while [in Top.Hoare2]
deterministic [in Top.Smallstep]
de_morgan_not_and_not [in Top.Logic]
div_mod_dec [in Top.Hoare2]
doit3times [in Top.Poly]
double [in Top.Induction]
double_negation_elimination [in Top.Logic]
dpow2_down [in Top.Hoare2]
drop [in Top.Norm]
E
empty [in Top.Maps]empty_pe_state [in Top.PE]
empty_state [in Top.Imp]
env [in Top.Norm]
equivalence [in Top.Rel]
equiv_classes [in Top.Equiv]
eq' [in Top.LibTactics]
evalF [in Top.Smallstep]
evenb [in Top.Basics]
even_1000 [in Top.Logic]
even_1000' [in Top.Logic]
even_1000'' [in Top.Logic]
ev_plus2 [in Top.ProofObjects]
ev_plus2' [in Top.ProofObjects]
ev_plus2'' [in Top.ProofObjects]
ev_plus4' [in Top.ProofObjects]
ev_plus4'' [in Top.ProofObjects]
ev_4''' [in Top.ProofObjects]
ev_8' [in Top.ProofObjects]
examplemap [in Top.Maps]
Examples.Employee [in Top.Sub]
Examples.Person [in Top.Sub]
Examples.Student [in Top.Sub]
Examples.subtyping_example_0 [in Top.Sub]
Examples.subtyping_example_0 [in Top.RecordSub]
Examples.subtyping_example_1 [in Top.Sub]
Examples.subtyping_example_1 [in Top.RecordSub]
Examples.subtyping_example_2 [in Top.Sub]
Examples.subtyping_example_2 [in Top.RecordSub]
Examples.subtyping_example_3 [in Top.RecordSub]
Examples.subtyping_example_4 [in Top.RecordSub]
Examples.sub_employee_person [in Top.Sub]
Examples.sub_student_person [in Top.Sub]
Examples.TRcd_j [in Top.RecordSub]
Examples.TRcd_kj [in Top.RecordSub]
Examples2.trcd_kj [in Top.RecordSub]
Examples2.typing_example_0 [in Top.RecordSub]
Examples2.typing_example_1 [in Top.RecordSub]
Examples2.typing_example_2 [in Top.RecordSub]
ExAssertions.as1 [in Top.Hoare]
ExAssertions.as2 [in Top.Hoare]
ExAssertions.as3 [in Top.Hoare]
ExAssertions.as4 [in Top.Hoare]
ExAssertions.as5 [in Top.Hoare]
ExAssertions.as6 [in Top.Hoare]
excluded_middle [in Top.Logic]
Exercises.Church.exp [in Top.Poly]
Exercises.Church.exp_1 [in Top.Poly]
Exercises.Church.exp_2 [in Top.Poly]
Exercises.Church.exp_3 [in Top.Poly]
Exercises.Church.mult [in Top.Poly]
Exercises.Church.mult_1 [in Top.Poly]
Exercises.Church.mult_2 [in Top.Poly]
Exercises.Church.mult_3 [in Top.Poly]
Exercises.Church.nat [in Top.Poly]
Exercises.Church.one [in Top.Poly]
Exercises.Church.plus [in Top.Poly]
Exercises.Church.plus_1 [in Top.Poly]
Exercises.Church.plus_2 [in Top.Poly]
Exercises.Church.plus_3 [in Top.Poly]
Exercises.Church.succ [in Top.Poly]
Exercises.Church.succ_1 [in Top.Poly]
Exercises.Church.succ_2 [in Top.Poly]
Exercises.Church.succ_3 [in Top.Poly]
Exercises.Church.three [in Top.Poly]
Exercises.Church.two [in Top.Poly]
Exercises.Church.zero [in Top.Poly]
Exercises.fold_length [in Top.Poly]
Exercises.fold_map [in Top.Poly]
Exercises.prod_curry [in Top.Poly]
Exercises.prod_uncurry [in Top.Poly]
Exercises.test_fold_length1 [in Top.Poly]
Exercises.test_map2 [in Top.Poly]
exp [in Top.Basics]
expect [in Top.ImpParser]
extract [in Top.Hoare2]
F
factorial [in Top.Basics]fact_in_coq [in Top.Imp]
filter [in Top.Poly]
filter_even_gt7 [in Top.Poly]
find_parity [in Top.Hoare2]
find_parity_dec [in Top.Hoare2]
find_parity_dec' [in Top.Hoare2]
firstExpect [in Top.ImpParser]
flat_map [in Top.Poly]
fold [in Top.Poly]
fold_aexp_ex1 [in Top.Equiv]
fold_aexp_ex2 [in Top.Equiv]
fold_bexp_ex1 [in Top.Equiv]
fold_bexp_ex2 [in Top.Equiv]
fold_com_ex1 [in Top.Equiv]
fold_constants_aexp [in Top.Equiv]
fold_constants_bexp [in Top.Equiv]
fold_constants_com [in Top.Equiv]
fold_example1 [in Top.Poly]
fold_example2 [in Top.Poly]
fold_example3 [in Top.Poly]
foo [in Top.Tactics]
forallb [in Top.Logic]
fst [in Top.Poly]
ftrue [in Top.Poly]
function_equality_ex [in Top.Logic]
H
halts [in Top.Norm]has_type_not [in Top.Types]
has_type_1 [in Top.Types]
hd_error [in Top.Poly]
Himp.cequiv [in Top.Equiv]
Himp.havoc_example1 [in Top.Equiv]
Himp.havoc_example2 [in Top.Equiv]
Himp.havoc_pre [in Top.Hoare]
Himp.hoare_triple [in Top.Hoare]
Himp.pcopy [in Top.Equiv]
Himp.ptwice [in Top.Equiv]
Himp.pXY [in Top.Equiv]
Himp.pYX [in Top.Equiv]
Himp.p1 [in Top.Equiv]
Himp.p2 [in Top.Equiv]
Himp.p3 [in Top.Equiv]
Himp.p4 [in Top.Equiv]
Himp.p5 [in Top.Equiv]
Himp.p6 [in Top.Equiv]
hoare_asgn_example1 [in Top.Hoare]
hoare_asgn_example1' [in Top.Hoare]
hoare_asgn_example3 [in Top.Hoare]
hoare_asgn_example4 [in Top.Hoare]
hoare_triple [in Top.Hoare]
I
If1.hoare_triple [in Top.Hoare]if_example [in Top.Hoare]
if_minus_dec [in Top.Hoare2]
if_minus_plus_com [in Top.Hoare2]
if_minus_plus_dec [in Top.Hoare2]
implies_to_or [in Top.Logic]
In [in Top.Logic]
inb [in Top.PE]
injective [in Top.Logic]
inversion_ex3 [in Top.Tactics]
inversion_ex6 [in Top.Tactics]
InvertsExamples.typing_nonexample_1 [in Top.UseTactics]
In_example_1 [in Top.Logic]
In_example_2 [in Top.Logic]
isAlpha [in Top.ImpParser]
isDigit [in Top.ImpParser]
isLowerAlpha [in Top.ImpParser]
isWhite [in Top.ImpParser]
is_even_prime [in Top.Logic]
is_fortytwo [in Top.Auto]
is_three [in Top.Logic]
is_wp [in Top.Hoare2]
K
keval [in Top.PE]keval_example [in Top.PE]
L
leb [in Top.Basics]lemma_application_ex [in Top.Logic]
length [in Top.Poly]
length_is_1 [in Top.Poly]
list123 [in Top.Poly]
list123' [in Top.Poly]
list123'' [in Top.Poly]
list123''' [in Top.Poly]
list_of_string [in Top.ImpParser]
lookup [in Top.Norm]
loop [in Top.Imp]
Loop.pe_loop_example1 [in Top.PE]
Loop.pe_loop_example2 [in Top.PE]
Loop.pe_loop_example3 [in Top.PE]
Loop.pe_loop_example4 [in Top.PE]
Loop.square_loop [in Top.PE]
lt [in Top.IndProp]
ltac_database [in Top.LibTactics]
ltac_nat_from_int [in Top.LibTactics]
ltac_something [in Top.LibTactics]
ltac_tag_subst [in Top.LibTactics]
ltac_to_generalize [in Top.LibTactics]
M
many [in Top.ImpParser]many_helper [in Top.ImpParser]
map [in Top.Poly]
minustwo [in Top.Basics]
msubst [in Top.Norm]
multistep [in Top.Types]
mupdate [in Top.Norm]
MyEquality.four' [in Top.ProofObjects]
MyEquality.singleton [in Top.ProofObjects]
myFact [in Top.UseAuto]
MyIff.iff [in Top.Logic]
mynil [in Top.Poly]
mynil [in Top.Poly]
mynil' [in Top.Poly]
MyNot.not [in Top.Logic]
N
nandb [in Top.Basics]NatList.add [in Top.Lists]
NatList.alternate [in Top.Lists]
NatList.app [in Top.Lists]
NatList.bag [in Top.Lists]
NatList.beq_natlist [in Top.Lists]
NatList.count [in Top.Lists]
NatList.countoddmembers [in Top.Lists]
NatList.fst [in Top.Lists]
NatList.fst' [in Top.Lists]
NatList.hd [in Top.Lists]
NatList.hd_error [in Top.Lists]
NatList.length [in Top.Lists]
NatList.member [in Top.Lists]
NatList.mylist [in Top.Lists]
NatList.mylist1 [in Top.Lists]
NatList.mylist2 [in Top.Lists]
NatList.mylist3 [in Top.Lists]
NatList.nonzeros [in Top.Lists]
NatList.nth_bad [in Top.Lists]
NatList.nth_error [in Top.Lists]
NatList.nth_error' [in Top.Lists]
NatList.oddmembers [in Top.Lists]
NatList.option_elim [in Top.Lists]
NatList.remove_all [in Top.Lists]
NatList.remove_one [in Top.Lists]
NatList.repeat [in Top.Lists]
NatList.rev [in Top.Lists]
NatList.snd [in Top.Lists]
NatList.snd' [in Top.Lists]
NatList.subset [in Top.Lists]
NatList.sum [in Top.Lists]
NatList.swap_pair [in Top.Lists]
NatList.test_add1 [in Top.Lists]
NatList.test_add2 [in Top.Lists]
NatList.test_alternate1 [in Top.Lists]
NatList.test_alternate2 [in Top.Lists]
NatList.test_alternate3 [in Top.Lists]
NatList.test_alternate4 [in Top.Lists]
NatList.test_app1 [in Top.Lists]
NatList.test_app2 [in Top.Lists]
NatList.test_app3 [in Top.Lists]
NatList.test_beq_natlist1 [in Top.Lists]
NatList.test_beq_natlist2 [in Top.Lists]
NatList.test_beq_natlist3 [in Top.Lists]
NatList.test_countoddmembers1 [in Top.Lists]
NatList.test_countoddmembers2 [in Top.Lists]
NatList.test_countoddmembers3 [in Top.Lists]
NatList.test_count1 [in Top.Lists]
NatList.test_count2 [in Top.Lists]
NatList.test_hd1 [in Top.Lists]
NatList.test_hd2 [in Top.Lists]
NatList.test_hd_error1 [in Top.Lists]
NatList.test_hd_error2 [in Top.Lists]
NatList.test_hd_error3 [in Top.Lists]
NatList.test_member1 [in Top.Lists]
NatList.test_member2 [in Top.Lists]
NatList.test_nonzeros [in Top.Lists]
NatList.test_nth_error1 [in Top.Lists]
NatList.test_nth_error2 [in Top.Lists]
NatList.test_nth_error3 [in Top.Lists]
NatList.test_oddmembers [in Top.Lists]
NatList.test_remove_all1 [in Top.Lists]
NatList.test_remove_all2 [in Top.Lists]
NatList.test_remove_all3 [in Top.Lists]
NatList.test_remove_all4 [in Top.Lists]
NatList.test_remove_one1 [in Top.Lists]
NatList.test_remove_one2 [in Top.Lists]
NatList.test_remove_one3 [in Top.Lists]
NatList.test_remove_one4 [in Top.Lists]
NatList.test_rev1 [in Top.Lists]
NatList.test_rev2 [in Top.Lists]
NatList.test_subset1 [in Top.Lists]
NatList.test_subset2 [in Top.Lists]
NatList.test_sum1 [in Top.Lists]
NatList.test_tl [in Top.Lists]
NatList.tl [in Top.Lists]
negb [in Top.Basics]
next_weekday [in Top.Basics]
normalizing [in Top.Smallstep]
normal_form [in Top.Smallstep]
normal_form_of [in Top.Smallstep]
no_whiles [in Top.Imp]
nth_error [in Top.Poly]
O
oddb [in Top.Basics]option_map [in Top.Poly]
orb [in Top.Basics]
order [in Top.Rel]
P
parity [in Top.Hoare2]parity [in Top.PE]
parity_body [in Top.PE]
parity_dec [in Top.Hoare2]
parity_eval [in Top.PE]
parse [in Top.ImpParser]
parseAExp [in Top.ImpParser]
parseAtomicExp [in Top.ImpParser]
parseBExp [in Top.ImpParser]
parseConjunctionExp [in Top.ImpParser]
parseIdentifier [in Top.ImpParser]
parseNumber [in Top.ImpParser]
parsePrimaryExp [in Top.ImpParser]
parseProductExp [in Top.ImpParser]
parser [in Top.ImpParser]
parseSequencedCommand [in Top.ImpParser]
parseSimpleCommand [in Top.ImpParser]
parseSumExp [in Top.ImpParser]
PartialMap.find [in Top.Lists]
PartialMap.update [in Top.Lists]
partial_function [in Top.Rel]
partial_map [in Top.Maps]
partition [in Top.Poly]
peirce [in Top.Logic]
pe_add [in Top.PE]
pe_aexp [in Top.PE]
pe_bexp [in Top.PE]
pe_block [in Top.PE]
pe_block_example [in Top.PE]
pe_compare [in Top.PE]
pe_consistent [in Top.PE]
pe_disagree_at [in Top.PE]
pe_example1 [in Top.PE]
pe_example2 [in Top.PE]
pe_example3 [in Top.PE]
pe_lookup [in Top.PE]
pe_program [in Top.PE]
pe_remove [in Top.PE]
pe_removes [in Top.PE]
pe_state [in Top.PE]
pe_unique [in Top.PE]
pe_update [in Top.PE]
Playground1.pred [in Top.Basics]
Playground2.minus [in Top.Basics]
Playground2.mult [in Top.Basics]
Playground2.plus [in Top.Basics]
Playground2.test_mult1 [in Top.Basics]
plus' [in Top.Basics]
plus2 [in Top.Imp]
plus3 [in Top.Poly]
plus_fact [in Top.Logic]
post [in Top.Hoare2]
pow2 [in Top.Hoare2]
pre [in Top.Hoare2]
preorder [in Top.Rel]
prog [in Top.Smallstep]
program [in Top.PE]
prog_a [in Top.Equiv]
prog_b [in Top.Equiv]
prog_c [in Top.Equiv]
prog_d [in Top.Equiv]
prog_e [in Top.Equiv]
prog_f [in Top.Equiv]
prog_g [in Top.Equiv]
prog_h [in Top.Equiv]
prog_i [in Top.Equiv]
Props.and_comm' [in Top.ProofObjects]
Props.and_comm'_aux [in Top.ProofObjects]
Props.conj_fact [in Top.ProofObjects]
Props.ex_ev_Sn [in Top.ProofObjects]
Props.or_comm [in Top.ProofObjects]
Props.some_nat_is_even [in Top.ProofObjects]
Pumping.napp [in Top.IndProp]
Pumping.pumping_constant [in Top.IndProp]
pup_to_n [in Top.ImpCEvalFun]
pup_to_n [in Top.Imp]
P_m0r [in Top.IndPrinciples]
P_m0r' [in Top.IndPrinciples]
Q
quiz6 [in Top.ProofObjects]R
R [in Top.Norm]real_fact [in Top.Hoare2]
reduce_to_zero' [in Top.Hoare2]
reflexive [in Top.Rel]
reg_exp_ex1 [in Top.IndProp]
reg_exp_ex2 [in Top.IndProp]
reg_exp_ex3 [in Top.IndProp]
reg_exp_ex4 [in Top.IndProp]
reg_exp_of_list [in Top.IndProp]
relation [in Top.Smallstep]
relation [in Top.Rel]
repeat [in Top.Poly]
RepeatExercise.ex1_repeat [in Top.Hoare]
RepeatExercise.hoare_triple [in Top.Hoare]
repeat' [in Top.Poly]
repeat'' [in Top.Poly]
repeat''' [in Top.Poly]
rev [in Top.Poly]
rev_append [in Top.Logic]
re_chars [in Top.IndProp]
re_not_empty [in Top.IndProp]
rm [in Top.LibTactics]
R.fR [in Top.IndProp]
S
sample_proof [in Top.HoareAsLogic]sillyfun [in Top.Tactics]
sillyfun1 [in Top.Tactics]
SimpleArith1.test_step_1 [in Top.Smallstep]
SimpleArith1.test_step_2 [in Top.Smallstep]
SkipExample.astep_example1 [in Top.UseTactics]
slow_assignment_dec [in Top.Hoare2]
snd [in Top.Poly]
some_term_is_stuck [in Top.Types]
split [in Top.Poly]
split_combine_statement [in Top.Tactics]
sqrt_dec [in Top.Hoare2]
square [in Top.Tactics]
square_dec [in Top.Hoare2]
square_dec' [in Top.Hoare2]
square_simpler_dec [in Top.Hoare2]
stack [in Top.Smallstep]
stack_multistep [in Top.Smallstep]
state [in Top.Imp]
step_normal_form [in Top.Smallstep]
STLCChecker.beq_ty [in Top.Typechecking]
STLCChecker.type_check [in Top.Typechecking]
STLCExtendedRecords.context [in Top.Records]
STLCExtendedRecords.FirstTry.alist [in Top.Records]
STLCExtendedRecords.subst [in Top.Records]
STLCExtendedRecords.tlookup [in Top.Records]
STLCExtendedRecords.Tlookup [in Top.Records]
STLCExtendedRecords.typing_nonexample [in Top.Records]
STLCExtendedRecords.typing_nonexample_2 [in Top.Records]
STLCExtendedRecords.weird_type [in Top.Records]
STLCExtended.context [in Top.MoreStlc]
STLCExtended.Examples.FixTest1.fact [in Top.MoreStlc]
STLCExtended.Examples.FixTest2.map [in Top.MoreStlc]
STLCExtended.Examples.FixTest3.equal [in Top.MoreStlc]
STLCExtended.Examples.FixTest4.eotest [in Top.MoreStlc]
STLCExtended.Examples.LetTest.test [in Top.MoreStlc]
STLCExtended.Examples.ListTest.test [in Top.MoreStlc]
STLCExtended.Examples.Numtest.test [in Top.MoreStlc]
STLCExtended.Examples.Prodtest.test [in Top.MoreStlc]
STLCExtended.Examples.Sumtest1.test [in Top.MoreStlc]
STLCExtended.Examples.Sumtest2.test [in Top.MoreStlc]
STLCExtended.subst [in Top.MoreStlc]
STLCProp.closed [in Top.StlcProp]
STLCProp.stuck [in Top.StlcProp]
STLCRef.context [in Top.References]
STLCRef.ExampleVariables.r [in Top.References]
STLCRef.ExampleVariables.s [in Top.References]
STLCRef.ExampleVariables.x [in Top.References]
STLCRef.ExampleVariables.y [in Top.References]
STLCRef.multistep [in Top.References]
STLCRef.preservation_theorem [in Top.References]
STLCRef.RefsAndNontermination.factorial [in Top.References]
STLCRef.RefsAndNontermination.loop [in Top.References]
STLCRef.RefsAndNontermination.loop_fun [in Top.References]
STLCRef.RefsAndNontermination.multistep1 [in Top.References]
STLCRef.replace [in Top.References]
STLCRef.store [in Top.References]
STLCRef.store_lookup [in Top.References]
STLCRef.store_Tlookup [in Top.References]
STLCRef.store_ty [in Top.References]
STLCRef.store_well_typed [in Top.References]
STLCRef.subst [in Top.References]
STLCRef.tseq [in Top.References]
STLC.context [in Top.Stlc]
STLC.subst [in Top.Stlc]
STLC.typing_example_1 [in Top.Stlc]
STLC.typing_example_1' [in Top.Stlc]
STLC.typing_example_2 [in Top.Stlc]
STLC.typing_example_2_full [in Top.Stlc]
STLC.typing_example_3 [in Top.Stlc]
STLC.typing_nonexample_1 [in Top.Stlc]
STLC.typing_nonexample_3 [in Top.Stlc]
STLC.x [in Top.Stlc]
STLC.y [in Top.Stlc]
STLC.z [in Top.Stlc]
string_of_list [in Top.ImpParser]
stuck [in Top.Types]
st12 [in Top.Auto]
st21 [in Top.Auto]
subst [in Top.Sub]
subst [in Top.Norm]
subst [in Top.RecordSub]
subst_aexp [in Top.Equiv]
subst_aexp_ex [in Top.Equiv]
subst_equiv_property [in Top.Equiv]
subtract_slowly [in Top.Imp]
subtract_slowly_body [in Top.Imp]
subtract_slowly_dec [in Top.Hoare2]
subtract_3_from_5_slowly [in Top.Imp]
succ_hastype_nat__hastype_nat [in Top.Types]
swap [in Top.Hoare2]
swap_dec [in Top.Hoare2]
swap_program [in Top.Hoare]
symmetric [in Top.Rel]
s_compile [in Top.Imp]
s_compile1 [in Top.Imp]
s_execute [in Top.Imp]
s_execute1 [in Top.Imp]
s_execute2 [in Top.Imp]
T
tass [in Top.Norm]Temp4.bool_step_prop1 [in Top.Smallstep]
Temp4.bool_step_prop2 [in Top.Smallstep]
Temp4.bool_step_prop3 [in Top.Smallstep]
Temp4.Temp5.bool_step_prop4 [in Top.Smallstep]
Temp4.Temp5.bool_step_prop4_holds [in Top.Smallstep]
testParsing [in Top.ImpParser]
test_andb31 [in Top.Basics]
test_andb32 [in Top.Basics]
test_andb33 [in Top.Basics]
test_andb34 [in Top.Basics]
test_anon_fun' [in Top.Poly]
test_blt_nat1 [in Top.Basics]
test_blt_nat2 [in Top.Basics]
test_blt_nat3 [in Top.Basics]
test_ceval [in Top.ImpCEvalFun]
test_countoddmembers'1 [in Top.Poly]
test_countoddmembers'2 [in Top.Poly]
test_countoddmembers'3 [in Top.Poly]
test_doit3times [in Top.Poly]
test_doit3times' [in Top.Poly]
test_factorial1 [in Top.Basics]
test_factorial2 [in Top.Basics]
test_filter1 [in Top.Poly]
test_filter2 [in Top.Poly]
test_filter2' [in Top.Poly]
test_filter_even_gt7_1 [in Top.Poly]
test_filter_even_gt7_2 [in Top.Poly]
test_flat_map1 [in Top.Poly]
test_hd_error1 [in Top.Poly]
test_hd_error2 [in Top.Poly]
test_leb1 [in Top.Basics]
test_leb2 [in Top.Basics]
test_leb3 [in Top.Basics]
test_length1 [in Top.Poly]
test_map1 [in Top.Poly]
test_map2 [in Top.Poly]
test_map3 [in Top.Poly]
test_nandb1 [in Top.Basics]
test_nandb2 [in Top.Basics]
test_nandb3 [in Top.Basics]
test_nandb4 [in Top.Basics]
test_next_weekday [in Top.Basics]
test_nostutter_1 [in Top.IndProp]
test_nostutter_2 [in Top.IndProp]
test_nostutter_3 [in Top.IndProp]
test_nostutter_4 [in Top.IndProp]
test_nth_error1 [in Top.Poly]
test_nth_error2 [in Top.Poly]
test_nth_error3 [in Top.Poly]
test_oddb1 [in Top.Basics]
test_oddb2 [in Top.Basics]
test_orb1 [in Top.Basics]
test_orb2 [in Top.Basics]
test_orb3 [in Top.Basics]
test_orb4 [in Top.Basics]
test_orb5 [in Top.Basics]
test_partition1 [in Top.Poly]
test_partition2 [in Top.Poly]
test_pe_aexp1 [in Top.PE]
test_pe_bexp1 [in Top.PE]
test_pe_bexp2 [in Top.PE]
test_pe_update [in Top.PE]
test_plus3 [in Top.Poly]
test_plus3' [in Top.Poly]
test_plus3'' [in Top.Poly]
test_repeat1 [in Top.Poly]
test_repeat2 [in Top.Poly]
test_rev1 [in Top.Poly]
test_rev2 [in Top.Poly]
test_split [in Top.Poly]
text_pe_aexp2 [in Top.PE]
tlookup [in Top.RecordSub]
Tlookup [in Top.RecordSub]
token [in Top.ImpParser]
tokenize [in Top.ImpParser]
tokenize_ex1 [in Top.ImpParser]
tokenize_helper [in Top.ImpParser]
total_map [in Top.Maps]
transitive [in Top.Rel]
trans_eq_example [in Top.Tactics]
trans_eq_example' [in Top.Tactics]
trans_eq_exercise [in Top.Tactics]
tr_rev [in Top.Logic]
two_loops_dec [in Top.Hoare2]
t_empty [in Top.Maps]
t_update [in Top.Maps]
U
update [in Top.Maps]update_example1 [in Top.Maps]
update_example2 [in Top.Maps]
update_example3 [in Top.Maps]
update_example4 [in Top.Maps]
V
value [in Top.Types]verification_conditions [in Top.Hoare2]
W
while_example [in Top.Hoare]wp [in Top.HoareAsLogic]
X
X [in Top.Imp]XtimesYinZ [in Top.Imp]
Y
Y [in Top.Imp]Z
Z [in Top.Imp]zprop [in Top.Equiv]
| Global Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | : | _ | (2854 entries) |
| Notation Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | : | _ | (174 entries) |
| Module Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | (81 entries) | |
| Variable Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | (8 entries) | |
| Library Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | (40 entries) | |
| Constructor Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | (854 entries) | |
| Lemma Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | (767 entries) | |
| Axiom Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | (12 entries) | |
| Inductive Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | (184 entries) | |
| Section Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | (3 entries) | |
| Abbreviation Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | (55 entries) | |
| Definition Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | (676 entries) |