| 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 | : | _ | (2518 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 | _ | (695 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 | _ | (4 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 | : | _ | (141 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 | _ | (727 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 | _ | (57 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 | _ | (179 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 | _ | (597 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) | |
| 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 | _ | (67 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 | _ | (31 entries) |
Global Index
A
abs_arrow [lemma, in Subtyping]abs_arrow [lemma, in RecordSub]
ACons [constructor, in ImpList]
add_slowly [definition, in Hoare]
admit [definition, in SfLib]
admit [definition, in Basics]
aequiv [definition, in Equiv]
aequiv_example [lemma, in Equiv]
aeval [definition, in ImpList]
aeval [definition, in Imp]
aeval_weakening [lemma, in Equiv]
aexp [inductive, in Imp]
aexp [inductive, in ImpList]
AExp [module, in Imp]
AExp.aeval [definition, in Imp]
AExp.aevalR [inductive, in Imp]
AExp.aevalR_first_try [module, in Imp]
AExp.aevalR_first_try.aevalR [inductive, in Imp]
AExp.aevalR_first_try.E_AMinus [constructor, in Imp]
AExp.aevalR_first_try.E_AMult [constructor, in Imp]
AExp.aevalR_first_try.E_ANum [constructor, in Imp]
AExp.aevalR_first_try.E_APlus [constructor, in Imp]
AExp.aevalR_first_try.:type_scope:x_'||'_x [notation, in Imp]
AExp.aeval_iff_aevalR [lemma, in Imp]
AExp.aeval_iff_aevalR' [lemma, in Imp]
AExp.aexp [inductive, in Imp]
AExp.AMinus [constructor, in Imp]
AExp.AMult [constructor, in Imp]
AExp.ANum [constructor, in Imp]
AExp.APlus [constructor, in Imp]
AExp.BAnd [constructor, in Imp]
AExp.BEq [constructor, in Imp]
AExp.beval [definition, in Imp]
AExp.bexp [inductive, in Imp]
AExp.BFalse [constructor, in Imp]
AExp.BLe [constructor, in Imp]
AExp.BNot [constructor, in Imp]
AExp.BTrue [constructor, in Imp]
AExp.E_AMinus [constructor, in Imp]
AExp.E_AMult [constructor, in Imp]
AExp.E_ANum [constructor, in Imp]
AExp.E_APlus [constructor, in Imp]
AExp.foo [lemma, in Imp]
AExp.foo' [lemma, in Imp]
AExp.optimize_0plus [definition, in Imp]
AExp.optimize_0plus_sound [lemma, in Imp]
AExp.optimize_0plus_sound' [lemma, in Imp]
AExp.optimize_0plus_sound'' [lemma, in Imp]
AExp.optimize_0plus_sound''' [lemma, in Imp]
AExp.silly_presburger_example [definition, in Imp]
AExp.test_aeval1 [definition, in Imp]
AExp.test_optimize_0plus [definition, in Imp]
AExp.:type_scope:x_'||'_x [notation, in Imp]
aexp1 [definition, in Imp]
afi_abs [constructor, in RecordSub]
afi_abs [constructor, in Norm]
afi_abs [constructor, in Subtyping]
afi_app1 [constructor, in RecordSub]
afi_app1 [constructor, in Subtyping]
afi_app1 [constructor, in Norm]
afi_app2 [constructor, in Subtyping]
afi_app2 [constructor, in Norm]
afi_app2 [constructor, in RecordSub]
afi_fst [constructor, in Norm]
afi_if0 [constructor, in Norm]
afi_if1 [constructor, in Subtyping]
afi_if1 [constructor, in Norm]
afi_if2 [constructor, in Norm]
afi_if2 [constructor, in Subtyping]
afi_if3 [constructor, in Subtyping]
afi_pair1 [constructor, in Norm]
afi_pair2 [constructor, in Norm]
afi_proj [constructor, in RecordSub]
afi_rhead [constructor, in RecordSub]
afi_rtail [constructor, in RecordSub]
afi_snd [constructor, in Norm]
afi_var [constructor, in RecordSub]
afi_var [constructor, in Subtyping]
afi_var [constructor, in Norm]
AHead [constructor, in ImpList]
AId [constructor, in ImpList]
AId [constructor, in Imp]
ai_here [constructor, in Logic]
ai_here [constructor, in SfLib]
ai_later [constructor, in SfLib]
ai_later [constructor, in Logic]
all [inductive, in Logic]
all3_spec [lemma, in Basics]
alpha [constructor, in ImpParser]
always_loop_hoare [lemma, in Hoare]
always_loop_hoare' [lemma, in Hoare]
AMinus [constructor, in Imp]
AMinus [constructor, in ImpList]
AMult [constructor, in ImpList]
AMult [constructor, in Imp]
and [inductive, in Logic]
andb [definition, in Basics]
andb3 [definition, in Basics]
andb_false [lemma, in Logic]
andb_false_r [lemma, in Basics]
andb_true [lemma, in SfLib]
andb_true_elim1 [lemma, in SfLib]
andb_true_elim1 [lemma, in Basics]
andb_true_elim2 [lemma, in SfLib]
andb_true_elim2 [lemma, in Basics]
andb_true__and [lemma, in Logic]
and_assoc [lemma, in Logic]
and_commut [lemma, in Logic]
and_example [lemma, in Logic]
and_example' [lemma, in Logic]
and__andb_true [lemma, in Logic]
ANil [constructor, in ImpList]
antisymmetric [definition, in Rel]
ANum [constructor, in Imp]
ANum [constructor, in ImpList]
APlus [constructor, in ImpList]
APlus [constructor, in Imp]
app [definition, in Poly]
appears_free_in [inductive, in RecordSub]
appears_free_in [inductive, in Norm]
appears_free_in [inductive, in Subtyping]
appears_in [inductive, in Logic]
appears_in [inductive, in SfLib]
appears_in_app [lemma, in Logic]
appears_in_app_split [lemma, in Logic]
appears_in_snoc1 [lemma, in Hoare]
appears_in_snoc2 [lemma, in Hoare]
appears_in_snoc3 [lemma, in Hoare]
append_nil [lemma, in Hoare]
append_singleton_equation [lemma, in Hoare]
app' [definition, in Poly]
app_appears_in [lemma, in Logic]
app_ass' [lemma, in Poly]
app_length [lemma, in Logic]
app_length_cons [lemma, in Gen]
app_length_twice [lemma, in Gen]
aslist [definition, in ImpList]
asnat [definition, in ImpList]
Assertion [definition, in Hoare]
assert_implies [definition, in Hoare]
Assign [constructor, in PE]
assign [definition, in PE]
assigned [definition, in PE]
assign_aequiv [lemma, in Equiv]
assign_removes [lemma, in PE]
assn_sub [definition, in Hoare]
assn_sub_example [definition, in Hoare]
assn_sub_example' [definition, in Hoare]
astep [inductive, in Smallstep]
astep_example1 [definition, in Types]
astep_example1' [definition, in Types]
astep_example1'' [definition, in Types]
astep_example1''' [definition, in Types]
astep_many [definition, in Types]
AS_Id [constructor, in Smallstep]
AS_Minus [constructor, in Smallstep]
AS_Minus1 [constructor, in Smallstep]
AS_Minus2 [constructor, in Smallstep]
AS_Mult [constructor, in Smallstep]
AS_Mult1 [constructor, in Smallstep]
AS_Mult2 [constructor, in Smallstep]
AS_Plus [constructor, in Smallstep]
AS_Plus1 [constructor, in Smallstep]
AS_Plus2 [constructor, in Smallstep]
ATail [constructor, in ImpList]
atrans_sound [definition, in Equiv]
auto_example_1 [lemma, in Types]
auto_example_2 [lemma, in Types]
auto_example_2a [lemma, in Types]
aval [inductive, in Smallstep]
av_num [constructor, in Smallstep]
B
BAnd [constructor, in ImpList]BAnd [constructor, in Imp]
Basics [library]
bassn [definition, in Hoare]
BEq [constructor, in ImpList]
BEq [constructor, in Imp]
bequiv [definition, in Equiv]
bequiv_example [lemma, in Equiv]
beq_false_not_eq [lemma, in Logic]
beq_id [definition, in ImpList]
beq_id [definition, in SfLib]
beq_id_eq [lemma, in SfLib]
beq_id_eq [lemma, in ImpList]
beq_id_false_not_eq [lemma, in SfLib]
beq_id_false_not_eq [lemma, in ImpList]
beq_id_refl [lemma, in ImpList]
beq_id_refl [lemma, in SfLib]
beq_id_sym [lemma, in SfLib]
beq_nat [definition, in Basics]
beq_nat_eq [lemma, in Poly]
beq_nat_eq' [lemma, in Poly]
beq_nat_refl [lemma, in Basics]
beq_nat_refl [lemma, in Hoare]
beq_nat_sym [lemma, in Poly]
beq_nat_sym [lemma, in SfLib]
beq_nat_trans [lemma, in Poly]
beq_nat_0_l [lemma, in Poly]
beq_nat_0_r [lemma, in Poly]
beq_true__eq [lemma, in Hoare]
between [definition, in Prop]
beval [definition, in ImpList]
beval [definition, in Imp]
bexp [inductive, in ImpList]
bexp [inductive, in Imp]
bexp1 [definition, in Imp]
bexp_eval_false [lemma, in Hoare]
bexp_eval_true [lemma, in Hoare]
BFalse [constructor, in ImpList]
BFalse [constructor, in Imp]
BIsCons [constructor, in ImpList]
BLe [constructor, in Imp]
BLe [constructor, in ImpList]
ble_nat [definition, in Basics]
ble_nat [definition, in SfLib]
ble_nat_false [lemma, in Logic]
ble_nat_false [lemma, in SfLib]
ble_nat_n_Sn_false [lemma, in Logic]
ble_nat_refl [lemma, in Basics]
ble_nat_true [lemma, in SfLib]
ble_nat_true [lemma, in Logic]
block [inductive, in PE]
blt_nat [definition, in Basics]
blue [constructor, in Prop]
BNot [constructor, in ImpList]
BNot [constructor, in Imp]
body [constructor, in PE]
bool [inductive, in Basics]
boollist [inductive, in Poly]
bool_cons [constructor, in Poly]
bool_nil [constructor, in Poly]
boxer [constructor, in LibTactics]
Boxer [inductive, in LibTactics]
bstep [inductive, in Smallstep]
BS_AndFalse [constructor, in Smallstep]
BS_AndStep [constructor, in Smallstep]
BS_AndTrueFalse [constructor, in Smallstep]
BS_AndTrueStep [constructor, in Smallstep]
BS_AndTrueTrue [constructor, in Smallstep]
BS_Eq [constructor, in Smallstep]
BS_Eq1 [constructor, in Smallstep]
BS_Eq2 [constructor, in Smallstep]
BS_LtEq [constructor, in Smallstep]
BS_LtEq1 [constructor, in Smallstep]
BS_LtEq2 [constructor, in Smallstep]
BS_NotFalse [constructor, in Smallstep]
BS_NotStep [constructor, in Smallstep]
BS_NotTrue [constructor, in Smallstep]
btrans_sound [definition, in Equiv]
BTrue [constructor, in ImpList]
BTrue [constructor, in Imp]
build_symtable [definition, in ImpParser]
bvalue [inductive, in Types]
bv_false [constructor, in Types]
bv_true [constructor, in Types]
C
canonical_forms_of_arrow_types [lemma, in RecordSub]canonical_forms_of_arrow_types [lemma, in Subtyping]
canonical_forms_of_Bool [lemma, in Subtyping]
CasesExample [module, in UseTactics]
CasesExample.update_same [lemma, in UseTactics]
CasesExample.update_same' [lemma, in UseTactics]
CAss [constructor, in Imp]
CAss [constructor, in ImpList]
CAss_congruence [lemma, in Equiv]
cequiv [definition, in Equiv]
cequiv' [definition, in Equiv]
cequiv__cequiv' [lemma, in Equiv]
ceval [inductive, in Imp]
ceval [inductive, in ImpList]
ceval' [inductive, in Equiv]
ceval_and_ceval_step_coincide [lemma, in Imp]
ceval_deterministic [lemma, in Imp]
ceval_deterministic' [lemma, in Imp]
ceval_example1 [definition, in Imp]
ceval_example2 [definition, in Imp]
ceval_extensionality [lemma, in PE]
ceval_step [definition, in Imp]
ceval_step1 [definition, in Imp]
ceval_step2 [definition, in Imp]
ceval_step3 [definition, in Imp]
ceval_step_more [lemma, in Imp]
ceval_step__ceval [lemma, in Imp]
ceval__ceval_step [lemma, in Imp]
chartype [inductive, in ImpParser]
CIf [constructor, in Imp]
CIf [constructor, in ImpList]
CIf_congruence [lemma, in Equiv]
CImp [module, in Smallstep]
CImp.CAss [constructor, in Smallstep]
CImp.CIf [constructor, in Smallstep]
CImp.com [inductive, in Smallstep]
CImp.CPar [constructor, in Smallstep]
CImp.CSeq [constructor, in Smallstep]
CImp.CSkip [constructor, in Smallstep]
CImp.cstep [inductive, in Smallstep]
CImp.cstepmany [definition, in Smallstep]
CImp.CS_Ass [constructor, in Smallstep]
CImp.CS_AssStep [constructor, in Smallstep]
CImp.CS_IfFalse [constructor, in Smallstep]
CImp.CS_IfStep [constructor, in Smallstep]
CImp.CS_IfTrue [constructor, in Smallstep]
CImp.CS_ParDone [constructor, in Smallstep]
CImp.CS_Par1 [constructor, in Smallstep]
CImp.CS_Par2 [constructor, in Smallstep]
CImp.CS_SeqFinish [constructor, in Smallstep]
CImp.CS_SeqStep [constructor, in Smallstep]
CImp.CS_While [constructor, in Smallstep]
CImp.CWhile [constructor, in Smallstep]
CImp.par_body_n [lemma, in Smallstep]
CImp.par_body_n__Sn [lemma, in Smallstep]
CImp.par_loop [definition, in Smallstep]
CImp.par_loop_any_X [lemma, in Smallstep]
CImp.par_loop_example_0 [definition, in Smallstep]
CImp.par_loop_example_2 [definition, in Smallstep]
CImp.::x_'/'_x_'==>'_x_'/'_x [notation, in Smallstep]
CImp.::x_'/'_x_'==>*'_x_'/'_x [notation, in Smallstep]
CImp.::x_'::='_x [notation, in Smallstep]
CImp.::x_';'_x [notation, in Smallstep]
CImp.::'IFB'_x_'THEN'_x_'ELSE'_x_'FI' [notation, in Smallstep]
CImp.::'PAR'_x_'WITH'_x_'END' [notation, in Smallstep]
CImp.::'SKIP' [notation, in Smallstep]
CImp.::'WHILE'_x_'DO'_x_'END' [notation, in Smallstep]
classic [definition, in Logic]
classic_double_neg [lemma, in Logic]
classifyChar [definition, in ImpParser]
closed [definition, in Norm]
closed_env [definition, in Norm]
clos_refl_trans [inductive, in Rel]
com [inductive, in Imp]
com [inductive, in ImpList]
combine [definition, in Poly]
Combined [module, in Smallstep]
Combined.step [inductive, in Smallstep]
Combined.ST_If [constructor, in Smallstep]
Combined.ST_IfFalse [constructor, in Smallstep]
Combined.ST_IfTrue [constructor, in Smallstep]
Combined.ST_PlusConstConst [constructor, in Smallstep]
Combined.ST_Plus1 [constructor, in Smallstep]
Combined.ST_Plus2 [constructor, in Smallstep]
Combined.tm [inductive, in Smallstep]
Combined.tm_const [constructor, in Smallstep]
Combined.tm_false [constructor, in Smallstep]
Combined.tm_if [constructor, in Smallstep]
Combined.tm_plus [constructor, in Smallstep]
Combined.tm_true [constructor, in Smallstep]
Combined.value [inductive, in Smallstep]
Combined.v_const [constructor, in Smallstep]
Combined.v_false [constructor, in Smallstep]
Combined.v_true [constructor, in Smallstep]
Combined.::x_'==>'_x [notation, in Smallstep]
combine' [definition, in Poly]
congruence_demo_1 [lemma, in UseAuto]
congruence_demo_2 [lemma, in UseAuto]
congruence_demo_3 [lemma, in UseAuto]
congruence_demo_4 [lemma, in UseAuto]
congruence_example [definition, in Equiv]
conj [constructor, in Logic]
conj_fact [definition, in Logic]
cons [constructor, in Poly]
constfun [definition, in Poly]
constfun_example1 [definition, in Poly]
constfun_example2 [definition, in Poly]
context [definition, in RecordSub]
context [definition, in Subtyping]
context [definition, in Norm]
context_invariance [lemma, in Norm]
context_invariance [lemma, in RecordSub]
context_invariance [lemma, in Subtyping]
contradiction_implies_anything [lemma, in Logic]
contrapositive [lemma, in Logic]
countoddmembers' [definition, in Poly]
CSeq [constructor, in Imp]
CSeq [constructor, in ImpList]
CSeq_congruence [lemma, in Equiv]
CSkip [constructor, in ImpList]
CSkip [constructor, in Imp]
cstep [inductive, in Smallstep]
CS_Ass [constructor, in Smallstep]
CS_AssStep [constructor, in Smallstep]
CS_IfFalse [constructor, in Smallstep]
CS_IfStep [constructor, in Smallstep]
CS_IfTrue [constructor, in Smallstep]
CS_SeqFinish [constructor, in Smallstep]
CS_SeqStep [constructor, in Smallstep]
CS_While [constructor, in Smallstep]
ctrans_sound [definition, in Equiv]
curry_uncurry [lemma, in Poly]
CWhile [constructor, in Imp]
CWhile [constructor, in ImpList]
CWhile_congruence [lemma, in Equiv]
C1 [constructor, in Prop]
C2 [constructor, in Prop]
D
day [inductive, in Basics]day_before [inductive, in Prop]
db_fri [constructor, in Prop]
db_mon [constructor, in Prop]
db_sat [constructor, in Prop]
db_sun [constructor, in Prop]
db_thu [constructor, in Prop]
db_tue [constructor, in Prop]
db_wed [constructor, in Prop]
DCAsgn [constructor, in Hoare]
DCIf [constructor, in Hoare]
dcom [inductive, in Hoare]
DCPost [constructor, in Hoare]
DCPre [constructor, in Hoare]
DCSeq [constructor, in Hoare]
DCSkip [constructor, in Hoare]
DCWhile [constructor, in Hoare]
dec_correct [definition, in Hoare]
dec_while [definition, in Hoare]
dec_while_correct [lemma, in Hoare]
DemoAbsurd1 [section, in UseAuto]
demo_auto_absurd_1 [lemma, in UseAuto]
demo_auto_absurd_2 [lemma, in UseAuto]
demo_false [lemma, in UseAuto]
demo_false [lemma, in UseTactics]
demo_false_arg [lemma, in UseTactics]
demo_hint_unfold_context_1 [lemma, in UseAuto]
demo_hint_unfold_context_2 [lemma, in UseAuto]
demo_hint_unfold_goal_1 [lemma, in UseAuto]
demo_hint_unfold_goal_2 [lemma, in UseAuto]
demo_tryfalse [lemma, in UseTactics]
DeterministicImp [module, in UseAuto]
DeterministicImp.ceval_deterministic [lemma, in UseAuto]
DeterministicImp.ceval_deterministic' [lemma, in UseAuto]
DeterministicImp.ceval_deterministic'' [lemma, in UseAuto]
DeterministicImp.ceval_deterministic''' [lemma, in UseAuto]
DeterministicImp.ceval_deterministic'''' [lemma, in UseAuto]
de_morgan_not_and_not [definition, in Logic]
digit [constructor, in ImpParser]
dist_exists_or [lemma, in Logic]
dist_not_exists [lemma, in Logic]
doit3times [definition, in Poly]
done [constructor, in PE]
double [definition, in Basics]
double_even [lemma, in Prop]
double_injective [lemma, in Poly]
double_injective' [lemma, in Gen]
double_injective_FAILED [lemma, in Gen]
double_injective_take2 [lemma, in Gen]
double_injective_take2_FAILED [lemma, in Gen]
double_neg [lemma, in Logic]
double_plus [lemma, in Basics]
drop [definition, in Norm]
duplicate_subst [lemma, in Norm]
dup_lemma [lemma, in LibTactics]
E
empty [definition, in RecordSub]empty [definition, in Subtyping]
empty [definition, in SfLib]
empty_pe_state [definition, in PE]
empty_relation [inductive, in SfLib]
empty_state [definition, in ImpList]
empty_state [definition, in Imp]
entry [constructor, in PE]
env [definition, in Norm]
EqualityExamples [module, in UseTactics]
EqualityExamples.big_expression_using [axiom, in UseTactics]
EqualityExamples.demo_applys_eq_1 [lemma, in UseTactics]
EqualityExamples.demo_applys_eq_2 [lemma, in UseTactics]
EqualityExamples.demo_applys_eq_3 [lemma, in UseTactics]
EqualityExamples.demo_fequals [lemma, in UseTactics]
EqualityExamples.demo_substs [lemma, in UseTactics]
EqualityExamples.mult_0_plus [lemma, in UseTactics]
EqualityExamples.mult_0_plus' [lemma, in UseTactics]
EqualityExamples.mult_0_plus'' [lemma, in UseTactics]
equality_by_auto [lemma, in UseAuto]
equatesLemma [section, in LibTactics]
equatesLemma.A0 [variable, in LibTactics]
equatesLemma.A1 [variable, in LibTactics]
equatesLemma.A2 [variable, in LibTactics]
equatesLemma.A3 [variable, in LibTactics]
equatesLemma.A4 [variable, in LibTactics]
equatesLemma.A5 [variable, in LibTactics]
equatesLemma.A6 [variable, in LibTactics]
equates_0 [lemma, in LibTactics]
equates_1 [lemma, in LibTactics]
equates_2 [lemma, in LibTactics]
equates_3 [lemma, in LibTactics]
equates_4 [lemma, in LibTactics]
equates_5 [lemma, in LibTactics]
equates_6 [lemma, in LibTactics]
Equiv [library]
equivalence [definition, in Rel]
eq' [definition, in LibTactics]
eq_add_S [lemma, in Poly]
eq_remove_S [lemma, in Poly]
ev [inductive, in Prop]
ev [inductive, in SfLib]
eval [inductive, in Smallstep]
eval_assign [lemma, in PE]
eval__stepmany [lemma, in Smallstep]
eval__value [lemma, in Smallstep]
even [definition, in Prop]
evenb [definition, in Basics]
evenb_n__oddb_Sn [lemma, in Basics]
even5_nonsense [lemma, in Prop]
even_ev [lemma, in Logic]
even_ev' [lemma, in Logic]
even_n__even_SSn [definition, in Prop]
ev_even [lemma, in Prop]
ev_even' [lemma, in Prop]
ev_ev_even [lemma, in Prop]
ev_minus2 [lemma, in Prop]
ev_minus2' [lemma, in Prop]
ev_MyProp [lemma, in Prop]
ev_MyProp' [lemma, in Prop]
ev_not_ev_S [lemma, in SfLib]
ev_not_ev_S [lemma, in Logic]
ev_plus4 [definition, in Prop]
ev_plus4' [lemma, in Prop]
ev_plus_plus [lemma, in Prop]
ev_SS [constructor, in Prop]
ev_SS [constructor, in SfLib]
ev_sum [lemma, in Prop]
ev_0 [constructor, in Prop]
ev_0 [constructor, in SfLib]
ex [inductive, in Logic]
Examples [module, in Subtyping]
Examples [module, in RecordSub]
ExamplesInstantiations [module, in UseTactics]
ExamplesInstantiations.substitution_preserves_typing [lemma, in UseTactics]
ExamplesLets [module, in UseTactics]
ExamplesLets.demo_lets_underscore [lemma, in UseTactics]
ExamplesLets.demo_lets_1 [lemma, in UseTactics]
ExamplesLets.demo_lets_2 [lemma, in UseTactics]
ExamplesLets.demo_lets_3 [lemma, in UseTactics]
ExamplesLets.demo_lets_4 [lemma, in UseTactics]
ExamplesLets.demo_lets_5 [lemma, in UseTactics]
ExamplesLets.typing_inversion_var [axiom, in UseTactics]
Examples.A [abbreviation, in RecordSub]
Examples.A [abbreviation, in Subtyping]
Examples.B [abbreviation, in RecordSub]
Examples.B [abbreviation, in Subtyping]
Examples.C [abbreviation, in RecordSub]
Examples.C [abbreviation, in Subtyping]
Examples.Employee [definition, in Subtyping]
Examples.Float [abbreviation, in Subtyping]
Examples.i [abbreviation, in RecordSub]
Examples.Integer [abbreviation, in Subtyping]
Examples.j [abbreviation, in RecordSub]
Examples.k [abbreviation, in RecordSub]
Examples.Person [definition, in Subtyping]
Examples.String [abbreviation, in Subtyping]
Examples.Student [definition, in Subtyping]
Examples.subtyping_example_0 [definition, in RecordSub]
Examples.subtyping_example_0 [definition, in Subtyping]
Examples.subtyping_example_1 [definition, in Subtyping]
Examples.subtyping_example_1 [definition, in RecordSub]
Examples.subtyping_example_2 [definition, in RecordSub]
Examples.subtyping_example_2 [definition, in Subtyping]
Examples.subtyping_example_3 [definition, in RecordSub]
Examples.subtyping_example_4 [definition, in RecordSub]
Examples.sub_employee_person [definition, in Subtyping]
Examples.sub_student_person [definition, in Subtyping]
Examples.tm_rcd_kj [definition, in RecordSub]
Examples.ty_rcd_j [definition, in RecordSub]
Examples.ty_rcd_kj [definition, in RecordSub]
Examples.x [abbreviation, in RecordSub]
Examples.x [abbreviation, in Subtyping]
Examples.y [abbreviation, in Subtyping]
Examples.y [abbreviation, in RecordSub]
Examples.z [abbreviation, in Subtyping]
Examples.z [abbreviation, in RecordSub]
Examples2 [module, in Subtyping]
Examples2 [module, in RecordSub]
Examples2.typing_example_0 [definition, in RecordSub]
Examples2.typing_example_1 [definition, in RecordSub]
Examples2.typing_example_2 [definition, in RecordSub]
excluded_middle [definition, in Logic]
existsb_app [lemma, in PE]
existsb_beq_id_filter [lemma, in PE]
exists_example_1 [definition, in Logic]
exists_example_1' [definition, in Logic]
exists_example_2 [lemma, in Logic]
exp [definition, in Basics]
expect [definition, in ImpParser]
ExSet [inductive, in Prop]
extend [definition, in Subtyping]
extend [definition, in SfLib]
extend [definition, in RecordSub]
extend_eq [lemma, in SfLib]
extend_neq [lemma, in SfLib]
extend_shadow [lemma, in SfLib]
extract [definition, in Hoare]
ex_falso_quodlibet [lemma, in Logic]
ex_falso_quodlibet [lemma, in SfLib]
ex_intro [constructor, in Logic]
E_Asgn [constructor, in ImpList]
E_Ass [constructor, in Imp]
E_Const [constructor, in Smallstep]
E_equiv [constructor, in Equiv]
E_IfFalse [constructor, in ImpList]
E_IfFalse [constructor, in Imp]
E_IfTrue [constructor, in ImpList]
E_IfTrue [constructor, in Imp]
E_None [constructor, in PE]
E_Plus [constructor, in Smallstep]
E_Seq [constructor, in Imp]
E_Seq [constructor, in ImpList]
E_Skip [constructor, in Imp]
E_Skip [constructor, in ImpList]
E_Some [constructor, in PE]
E_WhileEnd [constructor, in ImpList]
E_WhileEnd [constructor, in Imp]
E_WhileLoop [constructor, in Imp]
E_WhileLoop [constructor, in ImpList]
F
factorial [definition, in Basics]Factorial [module, in Hoare]
Factorial.fact_body [definition, in Hoare]
Factorial.fact_com [definition, in Hoare]
Factorial.fact_com_correct [lemma, in Hoare]
Factorial.fact_loop [definition, in Hoare]
Factorial.real_fact [definition, in Hoare]
fact_body [definition, in Imp]
fact_body_preserves_invariant [lemma, in Imp]
fact_com [definition, in Imp]
fact_com_correct [lemma, in Imp]
fact_invariant [definition, in Imp]
fact_in_coq [definition, in Imp]
fact_loop [definition, in Imp]
fact_loop_preserves_invariant [lemma, in Imp]
False [inductive, in Logic]
false [constructor, in Basics]
False_and_P_imp [lemma, in HoareAsLogic]
False_implies_nonsense [lemma, in Logic]
fdfs_any [constructor, in Prop]
fdfs_wed [lemma, in Prop]
fdfs_wed' [definition, in Prop]
filter [definition, in Poly]
filter_even_gt7 [definition, in Poly]
filter_exercise [lemma, in Poly]
find_parity [definition, in Hoare]
find_parity_correct [lemma, in Hoare]
find_parity_invariant [definition, in Hoare]
find_parity_invariant' [definition, in Hoare]
fine_day_for_singing [inductive, in Prop]
firstExpect [definition, in ImpParser]
five_not_even [lemma, in Logic]
flat_map [definition, in Poly]
fmostlytrue [definition, in Poly]
fold [definition, in Poly]
fold_aexp_ex1 [definition, in Equiv]
fold_aexp_ex2 [definition, in Equiv]
fold_bexp_ex1 [definition, in Equiv]
fold_bexp_ex2 [definition, in Equiv]
fold_com_ex1 [definition, in Equiv]
fold_constants_aexp [definition, in Equiv]
fold_constants_aexp_sound [lemma, in Equiv]
fold_constants_bexp [definition, in Equiv]
fold_constants_bexp_sound [lemma, in Equiv]
fold_constants_com [definition, in Equiv]
fold_constants_com_sound [lemma, in Equiv]
fold_example1 [definition, in Poly]
fold_example2 [definition, in Poly]
fold_example3 [definition, in Poly]
fold_length [definition, in Poly]
fold_length_correct [lemma, in Poly]
fold_map [definition, in Poly]
foo' [inductive, in Prop]
forallb [definition, in Logic]
four_ev [definition, in Prop]
four_ev' [lemma, in Prop]
free_in_context [lemma, in Subtyping]
free_in_context [lemma, in Norm]
free_in_context [lemma, in RecordSub]
friday [constructor, in Basics]
fst [definition, in Poly]
ftrue [definition, in Poly]
functional_extensionality [axiom, in Equiv]
funny_prop1 [definition, in Logic]
funny_prop1' [definition, in Logic]
funny_prop1'' [definition, in Logic]
G
gds [lemma, in Prop]gd_sat [constructor, in Prop]
gd_sun [constructor, in Prop]
Gen [library]
GenExample [module, in UseTactics]
GenExample.substitution_preserves_typing [lemma, in UseTactics]
good_day [inductive, in Prop]
Goto [constructor, in PE]
green [constructor, in Prop]
gt_not_le [axiom, in UseAuto]
guard_false_after_loop [lemma, in Imp]
H
halts [definition, in Norm]has_type [inductive, in RecordSub]
has_type [inductive, in Subtyping]
has_type [inductive, in Norm]
has_type [inductive, in Types]
has_type_not [definition, in Types]
has_type_1 [definition, in Types]
has_type__wf [lemma, in RecordSub]
hd_opt [definition, in Poly]
head [definition, in ImpList]
HintsTransitivity [section, in UseAuto]
Hoare [library]
HoareAsLogic [library]
hoare_asgn [lemma, in Hoare]
hoare_asgn_eq [lemma, in Hoare]
hoare_asgn_example1 [definition, in Hoare]
hoare_asgn_example1' [definition, in Hoare]
hoare_asgn_example3 [definition, in Hoare]
hoare_asgn_example4 [definition, in Hoare]
hoare_asgn_weakest [lemma, in Hoare]
hoare_consequence [lemma, in Hoare]
hoare_consequence_post [lemma, in Hoare]
hoare_consequence_pre [lemma, in Hoare]
hoare_if [lemma, in Hoare]
hoare_post_true [lemma, in Hoare]
hoare_pre_false [lemma, in Hoare]
hoare_proof [inductive, in HoareAsLogic]
hoare_proof_sound [lemma, in HoareAsLogic]
hoare_seq [lemma, in Hoare]
hoare_skip [lemma, in Hoare]
hoare_triple [definition, in Hoare]
hoare_while [lemma, in Hoare]
H_Asgn [constructor, in HoareAsLogic]
H_Consequence [constructor, in HoareAsLogic]
H_Consequence_post [constructor, in HoareAsLogic]
H_Consequence_pre [constructor, in HoareAsLogic]
H_If [constructor, in HoareAsLogic]
H_Post_True_deriv [lemma, in HoareAsLogic]
H_Pre_False_deriv [lemma, in HoareAsLogic]
H_Seq [constructor, in HoareAsLogic]
H_Skip [constructor, in HoareAsLogic]
H_While [constructor, in HoareAsLogic]
I
id [inductive, in ImpList]Id [constructor, in SfLib]
Id [module, in Imp]
Id [constructor, in ImpList]
id [inductive, in SfLib]
identity_assignment [lemma, in Equiv]
identity_assignment' [definition, in Equiv]
identity_assignment_first_try [lemma, in Equiv]
Id.beq_id [definition, in Imp]
Id.beq_id_eq [lemma, in Imp]
Id.beq_id_false_not_eq [lemma, in Imp]
Id.beq_id_refl [lemma, in Imp]
Id.beq_id_sym [lemma, in Imp]
Id.Id [constructor, in Imp]
Id.id [inductive, in Imp]
Id.not_eq_beq_id_false [lemma, in Imp]
If [constructor, in PE]
IFB_false [lemma, in Equiv]
IFB_true [lemma, in Equiv]
IFB_true_simple [lemma, in Equiv]
iff [definition, in Logic]
iff_implies [lemma, in Logic]
iff_intro_swap [lemma, in LibTactics]
iff_refl [lemma, in Logic]
iff_sym [lemma, in Logic]
iff_trans [lemma, in Logic]
iff_trans [lemma, in Equiv]
if_example [definition, in Hoare]
Imp [library]
implies_to_or [definition, in Logic]
ImpList [library]
ImpParser [library]
index [definition, in Poly]
index_after_last [lemma, in Gen]
inequiv_exercise [lemma, in Equiv]
inj_pair2 [axiom, in LibTactics]
instantiation [inductive, in Norm]
instantiation_domains_match [lemma, in Norm]
instantiation_drop [lemma, in Norm]
instantiation_env_closed [lemma, in Norm]
instantiation_R [lemma, in Norm]
IntrovExamples [module, in UseTactics]
IntrovExamples.ceval_and_ceval_step_coincide [lemma, in UseTactics]
IntrovExamples.ceval_deterministic [lemma, in UseTactics]
IntrovExamples.ceval_deterministic' [lemma, in UseTactics]
IntrovExamples.ceval_step__ceval [lemma, in UseTactics]
InvertsExamples [module, in UseTactics]
InvertsExamples.ceval_deterministic [lemma, in UseTactics]
InvertsExamples.ceval_deterministic' [lemma, in UseTactics]
InvertsExamples.skip_left [lemma, in UseTactics]
InvertsExamples.skip_left' [lemma, in UseTactics]
InvertsExamples.typing_nonexample_1 [definition, in UseTactics]
isAlpha [definition, in ImpParser]
isDigit [definition, in ImpParser]
isLowerAlpha [definition, in ImpParser]
isWhite [definition, in ImpParser]
K
keval [definition, in PE]keval_example [definition, in PE]
L
le [inductive, in Logic]leaf [constructor, in Prop]
LeFirstTry [module, in Logic]
LeFirstTry.le [inductive, in Logic]
LeFirstTry.le_n [constructor, in Logic]
LeFirstTry.le_S [constructor, in Logic]
length [definition, in Poly]
length' [definition, in Poly]
length'' [definition, in Poly]
length_is_1 [definition, in Poly]
length_snoc' [lemma, in Poly]
length_snoc''' [lemma, in Gen]
le_antisymmetric [lemma, in Rel]
le_gt_false [axiom, in UseAuto]
le_n [constructor, in Logic]
le_not_a_partial_function [lemma, in Rel]
le_not_gt [axiom, in UseAuto]
le_not_symmetric [lemma, in Rel]
le_order [lemma, in Rel]
le_plus_l [lemma, in Logic]
le_reflexive [lemma, in Rel]
le_S [constructor, in Logic]
le_Sn_le [lemma, in Rel]
le_Sn_n [lemma, in Rel]
le_step [lemma, in Rel]
le_S_n [lemma, in Rel]
le_trans [lemma, in Rel]
LibTactics [library]
LibTacticsCompatibility [module, in LibTactics]
list [inductive, in Poly]
Lists [library]
list123 [definition, in Poly]
list123' [definition, in Poly]
list123'' [definition, in Poly]
list123''' [definition, in Poly]
list_member [definition, in Hoare]
list_member_correct [lemma, in Hoare]
list_member_correct' [lemma, in Hoare]
list_member_dec [definition, in Hoare]
list_member_spec [definition, in Hoare]
list_of_string [definition, in ImpParser]
Logic [library]
lookup [definition, in Norm]
lookup_field_in_value [lemma, in RecordSub]
Loop [module, in PE]
loop [definition, in ImpList]
loop [constructor, in PE]
loop [definition, in Imp]
Loop.ceval_count [inductive, in PE]
Loop.ceval_count_complete [lemma, in PE]
Loop.ceval_count_sound [lemma, in PE]
Loop.E'Ass [constructor, in PE]
Loop.E'IfFalse [constructor, in PE]
Loop.E'IfTrue [constructor, in PE]
Loop.E'Seq [constructor, in PE]
Loop.E'Skip [constructor, in PE]
Loop.E'WhileEnd [constructor, in PE]
Loop.E'WhileLoop [constructor, in PE]
Loop.PE_AssDynamic [constructor, in PE]
Loop.PE_AssStatic [constructor, in PE]
Loop.pe_ceval_count [inductive, in PE]
Loop.pe_ceval_count_intro [constructor, in PE]
Loop.pe_ceval_count_le [lemma, in PE]
Loop.pe_com [inductive, in PE]
Loop.pe_compare_nil_lookup [lemma, in PE]
Loop.pe_compare_nil_override [lemma, in PE]
Loop.pe_com_complete [lemma, in PE]
Loop.pe_com_correct [lemma, in PE]
Loop.pe_com_sound [lemma, in PE]
Loop.PE_If [constructor, in PE]
Loop.PE_IfFalse [constructor, in PE]
Loop.PE_IfTrue [constructor, in PE]
Loop.pe_loop_example1 [definition, in PE]
Loop.pe_loop_example2 [definition, in PE]
Loop.pe_loop_example3 [definition, in PE]
Loop.pe_loop_example4 [definition, in PE]
Loop.PE_Seq [constructor, in PE]
Loop.PE_Skip [constructor, in PE]
Loop.PE_While [constructor, in PE]
Loop.PE_WhileEnd [constructor, in PE]
Loop.PE_WhileFixed [constructor, in PE]
Loop.PE_WhileFixedEnd [constructor, in PE]
Loop.PE_WhileFixedLoop [constructor, in PE]
Loop.PE_WhileLoop [constructor, in PE]
Loop.square_loop [definition, in PE]
Loop.::x_'/'_x_'/'_x_'/'_x_'||'_x_'#'_x [notation, in PE]
Loop.::x_'/'_x_'||'_x_'#'_x [notation, in PE]
Loop.::x_'/'_x_'||'_x_'/'_x_'/'_x [notation, in PE]
loop_never_stops [lemma, in Imp]
loop_never_stops [lemma, in ImpList]
loop_unrolling [lemma, in Equiv]
lt [definition, in Logic]
ltac_database [definition, in LibTactics]
ltac_database_provide [lemma, in LibTactics]
ltac_Mark [inductive, in LibTactics]
ltac_mark [constructor, in LibTactics]
ltac_nat_from_int [definition, in LibTactics]
ltac_no_arg [constructor, in LibTactics]
ltac_No_arg [inductive, in LibTactics]
ltac_something [definition, in LibTactics]
ltac_something_eq [lemma, in LibTactics]
ltac_something_hide [lemma, in LibTactics]
ltac_something_show [lemma, in LibTactics]
ltac_tag_subst [definition, in LibTactics]
ltac_to_generalize [definition, in LibTactics]
ltac_Wild [inductive, in LibTactics]
ltac_wild [constructor, in LibTactics]
ltac_wilds [constructor, in LibTactics]
ltac_Wilds [inductive, in LibTactics]
lt_S [lemma, in Logic]
lt_trans [lemma, in Rel]
lt_trans' [lemma, in Rel]
lt_trans'' [lemma, in Rel]
M
many [definition, in ImpParser]many_helper [definition, in ImpParser]
map [definition, in Poly]
map_rev [lemma, in Poly]
mextend [definition, in Norm]
mextend_drop [lemma, in Norm]
mextend_lookup [lemma, in Norm]
minustwo [definition, in Basics]
minus_diag [lemma, in Basics]
monday [constructor, in Basics]
MoreStlc [library]
msubst [definition, in Norm]
msubst_abs [lemma, in Norm]
msubst_app [lemma, in Norm]
msubst_closed [lemma, in Norm]
msubst_preserves_typing [lemma, in Norm]
msubst_R [lemma, in Norm]
msubst_var [lemma, in Norm]
mult_assoc [lemma, in Basics]
mult_comm [lemma, in Basics]
mult_plus_distr_r [lemma, in Basics]
mult_0_l [lemma, in Basics]
mult_0_plus [lemma, in Basics]
mult_0_plus' [lemma, in Basics]
mult_0_r [lemma, in Basics]
mult_0_r' [lemma, in Prop]
mult_0_r'' [lemma, in Prop]
mult_1_l [lemma, in Basics]
mult_1_plus [lemma, in Basics]
MumbleBaz [module, in Poly]
MumbleBaz.a [constructor, in Poly]
MumbleBaz.b [constructor, in Poly]
MumbleBaz.baz [inductive, in Poly]
MumbleBaz.c [constructor, in Poly]
MumbleBaz.d [constructor, in Poly]
MumbleBaz.e [constructor, in Poly]
MumbleBaz.grumble [inductive, in Poly]
MumbleBaz.mumble [inductive, in Poly]
MumbleBaz.x [constructor, in Poly]
MumbleBaz.y [constructor, in Poly]
MyEquality [module, in Logic]
MyEquality.eq [inductive, in Logic]
MyEquality.eq' [inductive, in Logic]
MyEquality.four [definition, in Logic]
MyEquality.refl_equal [constructor, in Logic]
MyEquality.refl_equal' [constructor, in Logic]
MyEquality.singleton [definition, in Logic]
MyEquality.two_defs_of_eq_coincide [lemma, in Logic]
MyEquality.:type_scope:x_'='''_x [notation, in Logic]
MyEquality.:type_scope:x_'='_x [notation, in Logic]
myFact [definition, in UseAuto]
mynil [definition, in Poly]
mynil' [definition, in Poly]
MyProp [inductive, in Prop]
MyProp1 [constructor, in Prop]
MyProp2 [constructor, in Prop]
MyProp3 [constructor, in Prop]
MyProp_ev [lemma, in Prop]
MyProp_iff_ev [definition, in Logic]
MyProp_plustwo [lemma, in Prop]
MyProp_ten [lemma, in Prop]
MyProp_0 [lemma, in Prop]
N
nandb [definition, in Basics]NaryExamples [module, in UseTactics]
NaryExamples.demo_branch [lemma, in UseTactics]
NaryExamples.demo_splits [lemma, in UseTactics]
NaryExamples.progress [lemma, in UseTactics]
NatList [module, in Lists]
natlist [inductive, in Prop]
NatList.add [definition, in Lists]
NatList.alternate [definition, in Lists]
NatList.app [definition, in Lists]
NatList.app_ass [lemma, in Lists]
NatList.app_ass4 [lemma, in Lists]
NatList.app_length [lemma, in Lists]
NatList.app_nil_end [lemma, in Lists]
NatList.bag [definition, in Lists]
NatList.beq_natlist [definition, in Lists]
NatList.beq_natlist_refl [lemma, in Lists]
NatList.ble_n_Sn [lemma, in Lists]
NatList.cons [constructor, in Lists]
NatList.count [definition, in Lists]
NatList.countoddmembers [definition, in Lists]
NatList.count_member_nonzero [lemma, in Lists]
NatList.Dictionary [module, in Lists]
NatList.Dictionary.dictionary [inductive, in Lists]
NatList.Dictionary.dictionary_invariant1 [lemma, in Lists]
NatList.Dictionary.dictionary_invariant2 [lemma, in Lists]
NatList.Dictionary.empty [constructor, in Lists]
NatList.Dictionary.find [definition, in Lists]
NatList.Dictionary.insert [definition, in Lists]
NatList.Dictionary.record [constructor, in Lists]
NatList.distr_rev [lemma, in Lists]
NatList.fst [definition, in Lists]
NatList.fst' [definition, in Lists]
NatList.fst_swap_is_snd [lemma, in Lists]
NatList.hd [definition, in Lists]
NatList.hd_opt [definition, in Lists]
NatList.index [definition, in Lists]
NatList.index' [definition, in Lists]
NatList.index_bad [definition, in Lists]
NatList.length [definition, in Lists]
NatList.length_snoc [lemma, in Lists]
NatList.l_123 [definition, in Lists]
NatList.l_123' [definition, in Lists]
NatList.l_123'' [definition, in Lists]
NatList.l_123''' [definition, in Lists]
NatList.member [definition, in Lists]
NatList.natlist [inductive, in Lists]
NatList.natoption [inductive, in Lists]
NatList.natprod [inductive, in Lists]
NatList.nil [constructor, in Lists]
NatList.nil_app [lemma, in Lists]
NatList.None [constructor, in Lists]
NatList.nonzeros [definition, in Lists]
NatList.nonzeros_length [lemma, in Lists]
NatList.oddmembers [definition, in Lists]
NatList.option_elim [definition, in Lists]
NatList.option_elim_hd [lemma, in Lists]
NatList.pair [constructor, in Lists]
NatList.remove_all [definition, in Lists]
NatList.remove_decreases_count [lemma, in Lists]
NatList.remove_one [definition, in Lists]
NatList.repeat [definition, in Lists]
NatList.rev [definition, in Lists]
NatList.rev_involutive [lemma, in Lists]
NatList.rev_length [lemma, in Lists]
NatList.rev_length_firsttry [lemma, in Lists]
NatList.snd [definition, in Lists]
NatList.snd' [definition, in Lists]
NatList.snd_fst_is_swap [lemma, in Lists]
NatList.snoc [definition, in Lists]
NatList.snoc_append [lemma, in Lists]
NatList.Some [constructor, in Lists]
NatList.subset [definition, in Lists]
NatList.sum [definition, in Lists]
NatList.surjective_pairing [lemma, in Lists]
NatList.surjective_pairing' [lemma, in Lists]
NatList.surjective_pairing_stuck [lemma, in Lists]
NatList.swap_pair [definition, in Lists]
NatList.tail [definition, in Lists]
NatList.test_add1 [definition, in Lists]
NatList.test_add2 [definition, in Lists]
NatList.test_alternate1 [definition, in Lists]
NatList.test_alternate2 [definition, in Lists]
NatList.test_alternate3 [definition, in Lists]
NatList.test_alternate4 [definition, in Lists]
NatList.test_app1 [definition, in Lists]
NatList.test_app2 [definition, in Lists]
NatList.test_app3 [definition, in Lists]
NatList.test_beq_natlist1 [definition, in Lists]
NatList.test_beq_natlist2 [definition, in Lists]
NatList.test_beq_natlist3 [definition, in Lists]
NatList.test_countoddmembers1 [definition, in Lists]
NatList.test_countoddmembers2 [definition, in Lists]
NatList.test_countoddmembers3 [definition, in Lists]
NatList.test_count1 [definition, in Lists]
NatList.test_count2 [definition, in Lists]
NatList.test_hd1 [definition, in Lists]
NatList.test_hd2 [definition, in Lists]
NatList.test_hd_opt1 [definition, in Lists]
NatList.test_hd_opt2 [definition, in Lists]
NatList.test_hd_opt3 [definition, in Lists]
NatList.test_index1 [definition, in Lists]
NatList.test_index2 [definition, in Lists]
NatList.test_index3 [definition, in Lists]
NatList.test_member1 [definition, in Lists]
NatList.test_member2 [definition, in Lists]
NatList.test_nonzeros [definition, in Lists]
NatList.test_oddmembers [definition, in Lists]
NatList.test_remove_all1 [definition, in Lists]
NatList.test_remove_all2 [definition, in Lists]
NatList.test_remove_all3 [definition, in Lists]
NatList.test_remove_all4 [definition, in Lists]
NatList.test_remove_one1 [definition, in Lists]
NatList.test_remove_one2 [definition, in Lists]
NatList.test_remove_one3 [definition, in Lists]
NatList.test_remove_one4 [definition, in Lists]
NatList.test_rev1 [definition, in Lists]
NatList.test_rev2 [definition, in Lists]
NatList.test_subset1 [definition, in Lists]
NatList.test_subset2 [definition, in Lists]
NatList.test_sum1 [definition, in Lists]
NatList.test_tail [definition, in Lists]
NatList.tl_length_pred [lemma, in Lists]
NatList.::x_'++'_x [notation, in Lists]
NatList.::x_'::'_x [notation, in Lists]
NatList.::'('_x_','_x_')' [notation, in Lists]
NatList.::'['_x_','_'..'_','_x_']' [notation, in Lists]
NatList.::'['_']' [notation, in Lists]
natlist1 [inductive, in Prop]
nat_ind2 [definition, in Logic]
ncons [constructor, in Prop]
negation_study_1 [lemma, in UseAuto]
negation_study_2 [lemma, in UseAuto]
negb [definition, in Basics]
negb_involutive [lemma, in Basics]
next_even [inductive, in Logic]
next_nat [inductive, in SfLib]
next_nat [inductive, in Logic]
next_nat_closure_is_le [lemma, in Rel]
next_nat_partial_function [lemma, in Rel]
next_weekday [definition, in Basics]
ne_1 [constructor, in Logic]
ne_2 [constructor, in Logic]
nf_is_value [lemma, in Smallstep]
nf_same_as_value [lemma, in Smallstep]
nil [constructor, in Poly]
nil_app [lemma, in Poly]
nn [constructor, in Logic]
nn [constructor, in SfLib]
nnil [constructor, in Prop]
nnil1 [constructor, in Prop]
no [constructor, in Prop]
node [constructor, in Prop]
None [constructor, in Poly]
NoneE [constructor, in ImpParser]
nonsense_implies_False [lemma, in Logic]
Norm [library]
normalization [lemma, in Norm]
normalizing [definition, in Smallstep]
normal_form [definition, in Smallstep]
normal_forms_unique [lemma, in Smallstep]
normal_form_of [definition, in Smallstep]
nostutter [inductive, in Logic]
not [definition, in Logic]
not_both_true_and_false [lemma, in Logic]
not_eq_beq_false [lemma, in Logic]
not_eq_beq_false [lemma, in SfLib]
not_eq_beq_id_false [lemma, in SfLib]
not_eq_beq_id_false [lemma, in ImpList]
not_ev_ev_S [lemma, in Hoare]
not_ev_ev_S_gen [lemma, in Hoare]
not_exists_dist [lemma, in Logic]
not_False [lemma, in Logic]
not_false_then_true [lemma, in Logic]
no_whiles [definition, in Imp]
no_whilesR [inductive, in Imp]
no_whiles_eqv [lemma, in Imp]
nsnoc1 [constructor, in Prop]
nvalue [inductive, in Types]
nv_succ [constructor, in Types]
nv_zero [constructor, in Types]
n_le_m__Sn_le_Sm [lemma, in Logic]
O
oddb [definition, in Basics]okdw [definition, in Prop]
okdw' [lemma, in Prop]
okd_before [constructor, in Prop]
okd_before2 [definition, in Prop]
okd_before2_valid [lemma, in Prop]
okd_before2_valid' [definition, in Prop]
okd_gd [constructor, in Prop]
ok_day [inductive, in Prop]
omega_demo_1 [lemma, in UseAuto]
omega_demo_2 [lemma, in UseAuto]
omega_demo_3 [lemma, in UseAuto]
omega_demo_4 [lemma, in UseAuto]
option [inductive, in Poly]
optionE [inductive, in ImpParser]
option_map [definition, in Poly]
or [inductive, in Logic]
orb [definition, in Basics]
orb_false [lemma, in Logic]
orb_true [lemma, in Logic]
order [definition, in Rel]
order_matters_1 [lemma, in UseAuto]
order_matters_2 [lemma, in UseAuto]
or_commut [lemma, in Logic]
or_commut' [lemma, in Logic]
or_distributes_over_and [lemma, in Logic]
or_distributes_over_and_1 [lemma, in Logic]
or_distributes_over_and_2 [lemma, in Logic]
or_introl [constructor, in Logic]
or_intror [constructor, in Logic]
other [constructor, in ImpParser]
our_nat_induction [definition, in Prop]
override [definition, in Poly]
override_eq [lemma, in Poly]
override_example [lemma, in Poly]
override_example1 [definition, in Poly]
override_example2 [definition, in Poly]
override_example3 [definition, in Poly]
override_example4 [definition, in Poly]
override_neq [lemma, in Poly]
override_permute [lemma, in Poly]
override_same [lemma, in Poly]
override_shadow [lemma, in Poly]
O_le_n [lemma, in Logic]
P
P [axiom, in UseAuto]P [module, in Prop]
p [definition, in Logic]
pair [constructor, in Poly]
parity [definition, in PE]
parity_body [definition, in PE]
parity_eval [definition, in PE]
parity_label [inductive, in PE]
parse [definition, in ImpParser]
parseAExp [definition, in ImpParser]
parseAtomicExp [definition, in ImpParser]
parseBExp [definition, in ImpParser]
parseConjunctionExp [definition, in ImpParser]
parseIdentifier [definition, in ImpParser]
parseNumber [definition, in ImpParser]
parsePrimaryExp [definition, in ImpParser]
parseProductExp [definition, in ImpParser]
parser [definition, in ImpParser]
parseSequencedCommand [definition, in ImpParser]
parseSimpleCommand [definition, in ImpParser]
parseSumExp [definition, in ImpParser]
partial_function [definition, in Rel]
partial_function [definition, in SfLib]
partial_map [definition, in SfLib]
partition [definition, in Poly]
PE [library]
peirce [definition, in Logic]
peval [inductive, in PE]
pe_add [definition, in PE]
pe_add_correct [lemma, in PE]
pe_aexp [definition, in PE]
pe_aexp_correct [lemma, in PE]
pe_aexp_correct_weak [lemma, in PE]
PE_AssDynamic [constructor, in PE]
PE_AssStatic [constructor, in PE]
pe_bexp [definition, in PE]
pe_bexp_correct [lemma, in PE]
pe_block [definition, in PE]
pe_block_correct [lemma, in PE]
pe_block_example [definition, in PE]
pe_ceval [inductive, in PE]
pe_ceval_intro [constructor, in PE]
pe_com [inductive, in PE]
pe_compare [definition, in PE]
pe_compare_correct [lemma, in PE]
pe_compare_override [lemma, in PE]
pe_compare_removes [lemma, in PE]
pe_com_complete [lemma, in PE]
pe_com_correct [lemma, in PE]
pe_com_sound [lemma, in PE]
pe_consistent [definition, in PE]
pe_consistent_override [lemma, in PE]
pe_disagree_at [definition, in PE]
pe_disagree_domain [lemma, in PE]
pe_domain [lemma, in PE]
pe_example1 [definition, in PE]
pe_example2 [definition, in PE]
pe_example3 [definition, in PE]
PE_If [constructor, in PE]
PE_IfFalse [constructor, in PE]
PE_IfTrue [constructor, in PE]
pe_lookup [definition, in PE]
pe_override [definition, in PE]
pe_override_consistent [lemma, in PE]
pe_override_correct [lemma, in PE]
pe_override_update_add [lemma, in PE]
pe_override_update_remove [lemma, in PE]
pe_peval [inductive, in PE]
pe_peval_intro [constructor, in PE]
pe_program [definition, in PE]
pe_program_correct [lemma, in PE]
pe_remove [definition, in PE]
pe_removes [definition, in PE]
pe_removes_correct [lemma, in PE]
pe_remove_correct [lemma, in PE]
PE_Seq [constructor, in PE]
PE_Skip [constructor, in PE]
pe_state [definition, in PE]
pe_unique [definition, in PE]
pe_unique_correct [lemma, in PE]
pigeonhole_principle [lemma, in Logic]
Playground1 [module, in Basics]
Playground1.nat [inductive, in Basics]
Playground1.O [constructor, in Basics]
Playground1.pred [definition, in Basics]
Playground1.S [constructor, in Basics]
Playground2 [module, in Basics]
Playground2.minus [definition, in Basics]
Playground2.mult [definition, in Basics]
Playground2.plus [definition, in Basics]
plus2 [definition, in Imp]
plus2_spec [lemma, in Imp]
plus3 [definition, in Poly]
plus_assoc [lemma, in Basics]
plus_assoc' [lemma, in Basics]
plus_assoc' [lemma, in Prop]
plus_ble_compat_l [lemma, in Basics]
plus_comm [lemma, in Basics]
plus_comm' [lemma, in Prop]
plus_comm'' [lemma, in Prop]
plus_fact [definition, in Prop]
plus_fact_is_true [lemma, in Prop]
plus_id_example [lemma, in Basics]
plus_id_exercise [lemma, in Basics]
plus_lt [lemma, in Logic]
plus_n_n_injective [lemma, in Poly]
plus_n_n_injective_take2 [lemma, in Gen]
plus_n_Sm [lemma, in Basics]
plus_one_r' [lemma, in Prop]
plus_O_n [lemma, in Basics]
plus_O_n' [lemma, in Basics]
plus_O_n'' [lemma, in Basics]
plus_rearrange [lemma, in Basics]
plus_rearrange_firsttry [lemma, in Basics]
plus_swap [lemma, in Basics]
plus_swap' [lemma, in Basics]
plus_0_r [lemma, in Basics]
plus_0_r_firsttry [lemma, in Basics]
plus_0_r_secondtry [lemma, in Basics]
plus_1_l [lemma, in Basics]
plus_1_neq_0 [lemma, in Basics]
plus_1_neq_0_firsttry [lemma, in Basics]
plus_2_2_is_4 [lemma, in Prop]
Poly [library]
post [definition, in Hoare]
Postscript [library]
pre [definition, in Hoare]
Preface [library]
preorder [definition, in Rel]
preservation [lemma, in Types]
preservation [lemma, in Subtyping]
preservation [lemma, in Norm]
preservation [lemma, in RecordSub]
PreservationProgressReferences [module, in UseAuto]
PreservationProgressReferences.nth_eq_snoc' [lemma, in UseAuto]
PreservationProgressReferences.preservation [lemma, in UseAuto]
PreservationProgressReferences.preservation' [lemma, in UseAuto]
PreservationProgressReferences.preservation_ref [lemma, in UseAuto]
PreservationProgressReferences.progress [lemma, in UseAuto]
PreservationProgressStlc [module, in UseAuto]
PreservationProgressStlc.preservation [lemma, in UseAuto]
PreservationProgressStlc.preservation' [lemma, in UseAuto]
PreservationProgressStlc.progress [lemma, in UseAuto]
PreservationProgressStlc.progress' [lemma, in UseAuto]
preservation' [lemma, in Types]
preserved_by_S [definition, in Prop]
prod [inductive, in Poly]
prod_curry [definition, in Poly]
prod_uncurry [definition, in Poly]
program [definition, in PE]
progress [lemma, in Subtyping]
progress [lemma, in Types]
progress [lemma, in RecordSub]
proj1 [lemma, in Logic]
proj2 [lemma, in Logic]
Prop [library]
pup_to_n [definition, in Imp]
P.c1 [constructor, in Prop]
P.c2 [constructor, in Prop]
P.c3 [constructor, in Prop]
P.p [inductive, in Prop]
P_m0r [definition, in Prop]
P_m0r' [definition, in Prop]
R
R [module, in Logic]R [definition, in Norm]
random_fact_1 [lemma, in Hoare]
random_fact_2 [lemma, in Hoare]
rcd_types_match [lemma, in RecordSub]
real_fact [definition, in Hoare]
real_fact [definition, in Imp]
Records [library]
RecordSub [library]
record_tm [inductive, in RecordSub]
record_ty [inductive, in RecordSub]
red [constructor, in Prop]
reduce_to_zero [definition, in Hoare]
reduce_to_zero_correct [lemma, in Hoare]
References [library]
reflexive [definition, in Rel]
refl_aequiv [lemma, in Equiv]
refl_bequiv [lemma, in Equiv]
refl_cequiv [lemma, in Equiv]
refl_step_closure [inductive, in Rel]
refl_step_closure [inductive, in SfLib]
Rel [library]
relation [definition, in Rel]
relation [definition, in SfLib]
repeat [definition, in Poly]
RepeatExercise [module, in Hoare]
RepeatExercise.CAss [constructor, in Hoare]
RepeatExercise.ceval [inductive, in Hoare]
RepeatExercise.CIf [constructor, in Hoare]
RepeatExercise.com [inductive, in Hoare]
RepeatExercise.CRepeat [constructor, in Hoare]
RepeatExercise.CSeq [constructor, in Hoare]
RepeatExercise.CSkip [constructor, in Hoare]
RepeatExercise.CWhile [constructor, in Hoare]
RepeatExercise.E_Ass [constructor, in Hoare]
RepeatExercise.E_IfFalse [constructor, in Hoare]
RepeatExercise.E_IfTrue [constructor, in Hoare]
RepeatExercise.E_Seq [constructor, in Hoare]
RepeatExercise.E_Skip [constructor, in Hoare]
RepeatExercise.E_WhileEnd [constructor, in Hoare]
RepeatExercise.E_WhileLoop [constructor, in Hoare]
RepeatExercise.hoare_triple [definition, in Hoare]
RepeatExercise.::x_'/'_x_'||'_x [notation, in Hoare]
RepeatExercise.::x_'::='_x [notation, in Hoare]
RepeatExercise.::x_';'_x [notation, in Hoare]
RepeatExercise.::'IFB'_x_'THEN'_x_'ELSE'_x_'FI' [notation, in Hoare]
RepeatExercise.::'REPEAT'_x_'UNTIL'_x_'END' [notation, in Hoare]
RepeatExercise.::'SKIP' [notation, in Hoare]
RepeatExercise.::'WHILE'_x_'DO'_x_'END' [notation, in Hoare]
RepeatExercise.::'{{'_x_'}}'_x_'{{'_x_'}}' [notation, in Hoare]
repeats [inductive, in Logic]
rev [definition, in Hoare]
rev [definition, in Poly]
rev_equation [lemma, in Hoare]
rev_exercise1 [lemma, in Poly]
rev_snoc [lemma, in Poly]
rgb [inductive, in Prop]
RingDemo [module, in UseAuto]
RingDemo.ring_demo [lemma, in UseAuto]
rm [definition, in LibTactics]
rsc_R [lemma, in SfLib]
rsc_R [lemma, in Rel]
rsc_refl [constructor, in SfLib]
rsc_refl [constructor, in Rel]
rsc_step [constructor, in SfLib]
rsc_step [constructor, in Rel]
rsc_trans [lemma, in SfLib]
rsc_trans [lemma, in Rel]
rtc_rsc_coincide [lemma, in Rel]
rtm_cons [constructor, in RecordSub]
rtm_nil [constructor, in RecordSub]
rty_cons [constructor, in RecordSub]
rty_nil [constructor, in RecordSub]
rt_refl [constructor, in Rel]
rt_step [constructor, in Rel]
rt_trans [constructor, in Rel]
R.c1 [constructor, in Logic]
R.c2 [constructor, in Logic]
R.c3 [constructor, in Logic]
R.c4 [constructor, in Logic]
R.c5 [constructor, in Logic]
R.R [inductive, in Logic]
R_halts [lemma, in Norm]
R_typable_empty [lemma, in Norm]
S
sample_proof [definition, in HoareAsLogic]saturday [constructor, in Basics]
search_depth_0 [lemma, in UseAuto]
search_depth_1 [lemma, in UseAuto]
search_depth_3 [lemma, in UseAuto]
search_depth_4 [lemma, in UseAuto]
search_depth_5 [lemma, in UseAuto]
Semantics [module, in UseAuto]
Semantics.stepmany__eval [lemma, in UseAuto]
Semantics.stepmany__eval' [lemma, in UseAuto]
seq_assoc [lemma, in Equiv]
SfLib [library]
sillyex1 [definition, in Poly]
sillyex2 [definition, in Poly]
sillyfun [definition, in Poly]
sillyfun1 [definition, in Poly]
sillyfun1_odd [lemma, in Poly]
sillyfun1_odd_FAILED [lemma, in Poly]
sillyfun_false [lemma, in Poly]
silly1 [lemma, in Poly]
silly2 [lemma, in Poly]
silly2a [lemma, in Poly]
silly3 [lemma, in Poly]
silly3' [lemma, in Poly]
silly3_firsttry [lemma, in Poly]
silly4 [lemma, in Poly]
silly5 [lemma, in Poly]
silly6 [lemma, in Poly]
silly7 [lemma, in Poly]
silly_ex [lemma, in Poly]
SimpleArith0 [module, in Smallstep]
SimpleArith0.eval [definition, in Smallstep]
SimpleArith1 [module, in Smallstep]
SimpleArith1.eval [inductive, in Smallstep]
SimpleArith1.E_Const [constructor, in Smallstep]
SimpleArith1.E_Plus [constructor, in Smallstep]
SimpleArith1.::x_'||'_x [notation, in Smallstep]
SimpleArith2 [module, in Smallstep]
SimpleArith2.step [inductive, in Smallstep]
SimpleArith2.step_deterministic [lemma, in Smallstep]
SimpleArith2.ST_PlusConstConst [constructor, in Smallstep]
SimpleArith2.ST_Plus1 [constructor, in Smallstep]
SimpleArith2.ST_Plus2 [constructor, in Smallstep]
SimpleArith2.test_step_1 [definition, in Smallstep]
SimpleArith2.test_step_2 [definition, in Smallstep]
SimpleArith2.::x_'==>'_x [notation, in Smallstep]
sinstr [inductive, in Imp]
SkipExample [module, in UseTactics]
SkipExample.astep_example1 [definition, in UseTactics]
SkipExample.ceval_deterministic [lemma, in UseTactics]
SkipExample.demo_skipH [lemma, in UseTactics]
SkipExample.mult_0_plus [lemma, in UseTactics]
skip_axiom [variable, in LibTactics]
skip_left [lemma, in Equiv]
skip_right [lemma, in Equiv]
SLoad [constructor, in Imp]
Smallstep [library]
SMinus [constructor, in Imp]
SMult [constructor, in Imp]
snd [definition, in Poly]
snie [definition, in Logic]
snoc [definition, in Hoare]
snoc [definition, in Poly]
snoc_equation [lemma, in Hoare]
snoc_with_append [lemma, in Poly]
Sn_le_Sm__n_le_m [lemma, in Logic]
solved_by_jauto [lemma, in UseAuto]
solving_by_apply [lemma, in UseAuto]
solving_by_apply' [lemma, in UseAuto]
solving_by_eapply [lemma, in UseAuto]
solving_by_reflexivity [lemma, in UseAuto]
solving_conj_goal [lemma, in UseAuto]
solving_conj_hyp [lemma, in UseAuto]
solving_conj_hyp' [lemma, in UseAuto]
solving_conj_hyp_forall [lemma, in UseAuto]
solving_conj_more [lemma, in UseAuto]
solving_disj_goal [lemma, in UseAuto]
solving_disj_hyp [lemma, in UseAuto]
solving_exists_goal [lemma, in UseAuto]
solving_exists_hyp [lemma, in UseAuto]
solving_tauto [lemma, in UseAuto]
Some [constructor, in Poly]
SomeE [constructor, in ImpParser]
some_nat_is_even [definition, in Logic]
some_tm_is_stuck [definition, in Types]
SortExamples [module, in UseTactics]
SortExamples.ceval_deterministic [lemma, in UseTactics]
soundness [lemma, in Types]
SPlus [constructor, in Imp]
SPush [constructor, in Imp]
sq [constructor, in Logic]
sqrt_com [definition, in Hoare]
sqrt_com_correct [lemma, in Hoare]
sqrt_inv [definition, in Hoare]
sqrt_loop [definition, in Hoare]
sqrt_spec [definition, in Hoare]
square_of [inductive, in Logic]
SSev_even [lemma, in Prop]
SSev_ev_firsttry [lemma, in Prop]
SSSSev_even [lemma, in Prop]
ss_invariant [definition, in Imp]
state [definition, in Imp]
state [definition, in ImpList]
step [inductive, in Norm]
step [inductive, in RecordSub]
step [inductive, in Smallstep]
step [inductive, in Subtyping]
step [inductive, in Types]
stepmany [abbreviation, in Norm]
stepmany [definition, in Types]
stepmany [definition, in Smallstep]
stepmany_App2 [lemma, in Norm]
stepmany_congr_1 [lemma, in Smallstep]
stepmany_congr_2 [lemma, in Smallstep]
stepmany_iff_eval [lemma, in Smallstep]
stepmany_preserves_R [lemma, in Norm]
stepmany_preserves_R' [lemma, in Norm]
stepmany__eval [lemma, in Smallstep]
step_deterministic [lemma, in Norm]
step_deterministic [lemma, in Smallstep]
step_deterministic [lemma, in Types]
step_normalizing [lemma, in Smallstep]
step_normal_form [definition, in Smallstep]
step_normal_form [abbreviation, in Norm]
step_normal_form [abbreviation, in Types]
step_preserves_halting [lemma, in Norm]
step_preserves_R [lemma, in Norm]
step_preserves_record_tm [lemma, in RecordSub]
step_preserves_R' [lemma, in Norm]
step__eval [lemma, in Smallstep]
stequiv [definition, in Equiv]
stequiv_aeval [lemma, in Equiv]
stequiv_beval [lemma, in Equiv]
stequiv_ceval [lemma, in Equiv]
stequiv_refl [lemma, in Equiv]
stequiv_sym [lemma, in Equiv]
stequiv_trans [lemma, in Equiv]
stequiv_update [lemma, in Equiv]
STLC [module, in Stlc]
Stlc [library]
STLCArith [module, in Stlc]
STLCArith.tm [inductive, in Stlc]
STLCArith.tm_abs [constructor, in Stlc]
STLCArith.tm_app [constructor, in Stlc]
STLCArith.tm_if0 [constructor, in Stlc]
STLCArith.tm_mult [constructor, in Stlc]
STLCArith.tm_nat [constructor, in Stlc]
STLCArith.tm_pred [constructor, in Stlc]
STLCArith.tm_succ [constructor, in Stlc]
STLCArith.tm_var [constructor, in Stlc]
STLCArith.ty [inductive, in Stlc]
STLCArith.ty_arrow [constructor, in Stlc]
STLCArith.ty_Nat [constructor, in Stlc]
STLCChecker [module, in Typechecking]
STLCChecker.beq_ty [definition, in Typechecking]
STLCChecker.beq_ty_refl [lemma, in Typechecking]
STLCChecker.beq_ty__eq [lemma, in Typechecking]
STLCChecker.type_check [definition, in Typechecking]
STLCChecker.type_checking_complete [lemma, in Typechecking]
STLCChecker.type_checking_sound [lemma, in Typechecking]
STLCExtended [module, in MoreStlc]
STLCExtendedRecords [module, in Records]
STLCExtendedRecords.a [abbreviation, in Records]
STLCExtendedRecords.A [abbreviation, in Records]
STLCExtendedRecords.afi_abs [constructor, in Records]
STLCExtendedRecords.afi_app1 [constructor, in Records]
STLCExtendedRecords.afi_app2 [constructor, in Records]
STLCExtendedRecords.afi_proj [constructor, in Records]
STLCExtendedRecords.afi_rhead [constructor, in Records]
STLCExtendedRecords.afi_rtail [constructor, in Records]
STLCExtendedRecords.afi_var [constructor, in Records]
STLCExtendedRecords.appears_free_in [inductive, in Records]
STLCExtendedRecords.B [abbreviation, in Records]
STLCExtendedRecords.context [definition, in Records]
STLCExtendedRecords.context_invariance [lemma, in Records]
STLCExtendedRecords.f [abbreviation, in Records]
STLCExtendedRecords.FirstTry [module, in Records]
STLCExtendedRecords.FirstTry.alist [definition, in Records]
STLCExtendedRecords.FirstTry.ty [inductive, in Records]
STLCExtendedRecords.FirstTry.ty_arrow [constructor, in Records]
STLCExtendedRecords.FirstTry.ty_base [constructor, in Records]
STLCExtendedRecords.FirstTry.ty_rcd [constructor, in Records]
STLCExtendedRecords.free_in_context [lemma, in Records]
STLCExtendedRecords.g [abbreviation, in Records]
STLCExtendedRecords.has_type [inductive, in Records]
STLCExtendedRecords.has_type__wf [lemma, in Records]
STLCExtendedRecords.i1 [abbreviation, in Records]
STLCExtendedRecords.i2 [abbreviation, in Records]
STLCExtendedRecords.k [abbreviation, in Records]
STLCExtendedRecords.l [abbreviation, in Records]
STLCExtendedRecords.lookup_field_in_value [lemma, in Records]
STLCExtendedRecords.preservation [lemma, in Records]
STLCExtendedRecords.progress [lemma, in Records]
STLCExtendedRecords.record_tm [inductive, in Records]
STLCExtendedRecords.record_ty [inductive, in Records]
STLCExtendedRecords.rtm_cons [constructor, in Records]
STLCExtendedRecords.rtm_nil [constructor, in Records]
STLCExtendedRecords.rty_cons [constructor, in Records]
STLCExtendedRecords.rty_nil [constructor, in Records]
STLCExtendedRecords.step [inductive, in Records]
STLCExtendedRecords.stepmany [abbreviation, in Records]
STLCExtendedRecords.step_preserves_record_tm [lemma, in Records]
STLCExtendedRecords.ST_AppAbs [constructor, in Records]
STLCExtendedRecords.ST_App1 [constructor, in Records]
STLCExtendedRecords.ST_App2 [constructor, in Records]
STLCExtendedRecords.ST_ProjRcd [constructor, in Records]
STLCExtendedRecords.ST_Proj1 [constructor, in Records]
STLCExtendedRecords.ST_Rcd_Head [constructor, in Records]
STLCExtendedRecords.ST_Rcd_Tail [constructor, in Records]
STLCExtendedRecords.subst [definition, in Records]
STLCExtendedRecords.substitution_preserves_typing [lemma, in Records]
STLCExtendedRecords.tm [inductive, in Records]
STLCExtendedRecords.tm_abs [constructor, in Records]
STLCExtendedRecords.tm_app [constructor, in Records]
STLCExtendedRecords.tm_lookup [definition, in Records]
STLCExtendedRecords.tm_proj [constructor, in Records]
STLCExtendedRecords.tm_rcons [constructor, in Records]
STLCExtendedRecords.tm_rnil [constructor, in Records]
STLCExtendedRecords.tm_var [constructor, in Records]
STLCExtendedRecords.ty [inductive, in Records]
STLCExtendedRecords.typing_example_2 [lemma, in Records]
STLCExtendedRecords.typing_nonexample [definition, in Records]
STLCExtendedRecords.typing_nonexample_2 [definition, in Records]
STLCExtendedRecords.ty_arrow [constructor, in Records]
STLCExtendedRecords.ty_base [constructor, in Records]
STLCExtendedRecords.ty_lookup [definition, in Records]
STLCExtendedRecords.ty_rcons [constructor, in Records]
STLCExtendedRecords.ty_rnil [constructor, in Records]
STLCExtendedRecords.T_Abs [constructor, in Records]
STLCExtendedRecords.T_App [constructor, in Records]
STLCExtendedRecords.T_Proj [constructor, in Records]
STLCExtendedRecords.T_RCons [constructor, in Records]
STLCExtendedRecords.T_RNil [constructor, in Records]
STLCExtendedRecords.T_Var [constructor, in Records]
STLCExtendedRecords.value [inductive, in Records]
STLCExtendedRecords.v_abs [constructor, in Records]
STLCExtendedRecords.v_rcons [constructor, in Records]
STLCExtendedRecords.v_rnil [constructor, in Records]
STLCExtendedRecords.weird_type [definition, in Records]
STLCExtendedRecords.well_formed_ty [inductive, in Records]
STLCExtendedRecords.wfty_arrow [constructor, in Records]
STLCExtendedRecords.wfty_base [constructor, in Records]
STLCExtendedRecords.wfty_rcons [constructor, in Records]
STLCExtendedRecords.wfty_rnil [constructor, in Records]
STLCExtendedRecords.wf_rcd_lookup [lemma, in Records]
STLCExtendedRecords.::x_'==>'_x [notation, in Records]
STLCExtendedRecords.::x_'==>*'_x [notation, in Records]
STLCExtended.afi_abs [constructor, in MoreStlc]
STLCExtended.afi_app1 [constructor, in MoreStlc]
STLCExtended.afi_app2 [constructor, in MoreStlc]
STLCExtended.afi_var [constructor, in MoreStlc]
STLCExtended.appears_free_in [inductive, in MoreStlc]
STLCExtended.context [definition, in MoreStlc]
STLCExtended.context_invariance [lemma, in MoreStlc]
STLCExtended.Examples [module, in MoreStlc]
STLCExtended.Examples.a [abbreviation, in MoreStlc]
STLCExtended.Examples.eo [abbreviation, in MoreStlc]
STLCExtended.Examples.eq [abbreviation, in MoreStlc]
STLCExtended.Examples.even [abbreviation, in MoreStlc]
STLCExtended.Examples.evenodd [abbreviation, in MoreStlc]
STLCExtended.Examples.f [abbreviation, in MoreStlc]
STLCExtended.Examples.FixTest1 [module, in MoreStlc]
STLCExtended.Examples.FixTest1.fact [definition, in MoreStlc]
STLCExtended.Examples.FixTest2 [module, in MoreStlc]
STLCExtended.Examples.FixTest2.map [definition, in MoreStlc]
STLCExtended.Examples.FixTest3 [module, in MoreStlc]
STLCExtended.Examples.FixTest3.equal [definition, in MoreStlc]
STLCExtended.Examples.FixTest4 [module, in MoreStlc]
STLCExtended.Examples.FixTest4.eotest [definition, in MoreStlc]
STLCExtended.Examples.g [abbreviation, in MoreStlc]
STLCExtended.Examples.i1 [abbreviation, in MoreStlc]
STLCExtended.Examples.i2 [abbreviation, in MoreStlc]
STLCExtended.Examples.k [abbreviation, in MoreStlc]
STLCExtended.Examples.l [abbreviation, in MoreStlc]
STLCExtended.Examples.LetTest [module, in MoreStlc]
STLCExtended.Examples.LetTest.test [definition, in MoreStlc]
STLCExtended.Examples.ListTest [module, in MoreStlc]
STLCExtended.Examples.ListTest.test [definition, in MoreStlc]
STLCExtended.Examples.m [abbreviation, in MoreStlc]
STLCExtended.Examples.n [abbreviation, in MoreStlc]
STLCExtended.Examples.Numtest [module, in MoreStlc]
STLCExtended.Examples.Numtest.test [definition, in MoreStlc]
STLCExtended.Examples.odd [abbreviation, in MoreStlc]
STLCExtended.Examples.processSum [abbreviation, in MoreStlc]
STLCExtended.Examples.Prodtest [module, in MoreStlc]
STLCExtended.Examples.Prodtest.test [definition, in MoreStlc]
STLCExtended.Examples.Sumtest1 [module, in MoreStlc]
STLCExtended.Examples.Sumtest1.test [definition, in MoreStlc]
STLCExtended.Examples.Sumtest2 [module, in MoreStlc]
STLCExtended.Examples.Sumtest2.test [definition, in MoreStlc]
STLCExtended.Examples.x [abbreviation, in MoreStlc]
STLCExtended.Examples.y [abbreviation, in MoreStlc]
STLCExtended.free_in_context [lemma, in MoreStlc]
STLCExtended.has_type [inductive, in MoreStlc]
STLCExtended.preservation [lemma, in MoreStlc]
STLCExtended.progress [lemma, in MoreStlc]
STLCExtended.step [inductive, in MoreStlc]
STLCExtended.stepmany [abbreviation, in MoreStlc]
STLCExtended.ST_AppAbs [constructor, in MoreStlc]
STLCExtended.ST_App1 [constructor, in MoreStlc]
STLCExtended.ST_App2 [constructor, in MoreStlc]
STLCExtended.subst [definition, in MoreStlc]
STLCExtended.substitution_preserves_typing [lemma, in MoreStlc]
STLCExtended.tm [inductive, in MoreStlc]
STLCExtended.tm_abs [constructor, in MoreStlc]
STLCExtended.tm_app [constructor, in MoreStlc]
STLCExtended.tm_case [constructor, in MoreStlc]
STLCExtended.tm_cons [constructor, in MoreStlc]
STLCExtended.tm_fix [constructor, in MoreStlc]
STLCExtended.tm_fst [constructor, in MoreStlc]
STLCExtended.tm_if0 [constructor, in MoreStlc]
STLCExtended.tm_inl [constructor, in MoreStlc]
STLCExtended.tm_inr [constructor, in MoreStlc]
STLCExtended.tm_lcase [constructor, in MoreStlc]
STLCExtended.tm_let [constructor, in MoreStlc]
STLCExtended.tm_mult [constructor, in MoreStlc]
STLCExtended.tm_nat [constructor, in MoreStlc]
STLCExtended.tm_nil [constructor, in MoreStlc]
STLCExtended.tm_pair [constructor, in MoreStlc]
STLCExtended.tm_pred [constructor, in MoreStlc]
STLCExtended.tm_snd [constructor, in MoreStlc]
STLCExtended.tm_succ [constructor, in MoreStlc]
STLCExtended.tm_var [constructor, in MoreStlc]
STLCExtended.ty [inductive, in MoreStlc]
STLCExtended.ty_arrow [constructor, in MoreStlc]
STLCExtended.ty_List [constructor, in MoreStlc]
STLCExtended.ty_Nat [constructor, in MoreStlc]
STLCExtended.ty_prod [constructor, in MoreStlc]
STLCExtended.ty_sum [constructor, in MoreStlc]
STLCExtended.T_Abs [constructor, in MoreStlc]
STLCExtended.T_App [constructor, in MoreStlc]
STLCExtended.T_Var [constructor, in MoreStlc]
STLCExtended.value [inductive, in MoreStlc]
STLCExtended.v_abs [constructor, in MoreStlc]
STLCExtended.::x_'==>'_x [notation, in MoreStlc]
STLCExtended.::x_'==>*'_x [notation, in MoreStlc]
STLCRef [module, in References]
STLCRef.afi_abs [constructor, in References]
STLCRef.afi_app1 [constructor, in References]
STLCRef.afi_app2 [constructor, in References]
STLCRef.afi_assign1 [constructor, in References]
STLCRef.afi_assign2 [constructor, in References]
STLCRef.afi_deref [constructor, in References]
STLCRef.afi_if0_1 [constructor, in References]
STLCRef.afi_if0_2 [constructor, in References]
STLCRef.afi_if0_3 [constructor, in References]
STLCRef.afi_mult1 [constructor, in References]
STLCRef.afi_mult2 [constructor, in References]
STLCRef.afi_pred [constructor, in References]
STLCRef.afi_ref [constructor, in References]
STLCRef.afi_succ [constructor, in References]
STLCRef.afi_var [constructor, in References]
STLCRef.appears_free_in [inductive, in References]
STLCRef.assign_pres_store_typing [lemma, in References]
STLCRef.context [definition, in References]
STLCRef.context_invariance [lemma, in References]
STLCRef.ExampleVariables [module, in References]
STLCRef.ExampleVariables.r [definition, in References]
STLCRef.ExampleVariables.s [definition, in References]
STLCRef.ExampleVariables.x [definition, in References]
STLCRef.ExampleVariables.y [definition, in References]
STLCRef.extends [inductive, in References]
STLCRef.extends_cons [constructor, in References]
STLCRef.extends_lookup [lemma, in References]
STLCRef.extends_nil [constructor, in References]
STLCRef.extends_refl [lemma, in References]
STLCRef.extends_snoc [lemma, in References]
STLCRef.factorial [definition, in References]
STLCRef.factorial_type [lemma, in References]
STLCRef.free_in_context [lemma, in References]
STLCRef.has_type [inductive, in References]
STLCRef.length_extends [lemma, in References]
STLCRef.length_replace [lemma, in References]
STLCRef.length_snoc [lemma, in References]
STLCRef.lookup_replace_eq [lemma, in References]
STLCRef.lookup_replace_neq [lemma, in References]
STLCRef.loop [definition, in References]
STLCRef.loop_fun [definition, in References]
STLCRef.loop_fun_step_self [lemma, in References]
STLCRef.loop_steps_to_loop_fun [lemma, in References]
STLCRef.loop_typeable [lemma, in References]
STLCRef.nth_eq_snoc [lemma, in References]
STLCRef.nth_lt_snoc [lemma, in References]
STLCRef.preservation [lemma, in References]
STLCRef.preservation_theorem [definition, in References]
STLCRef.preservation_wrong1 [lemma, in References]
STLCRef.preservation_wrong2 [lemma, in References]
STLCRef.progress [lemma, in References]
STLCRef.RefsAndNontermination [section, in References]
STLCRef.RefsAndNontermination.::x_'/'_x_'==>+'_x_'/'_x [notation, in References]
STLCRef.replace [definition, in References]
STLCRef.replace_nil [lemma, in References]
STLCRef.sc_one [constructor, in References]
STLCRef.sc_step [constructor, in References]
STLCRef.snoc [definition, in References]
STLCRef.step [inductive, in References]
STLCRef.stepmany [definition, in References]
STLCRef.stepmany1 [definition, in References]
STLCRef.step_closure [inductive, in References]
STLCRef.store [definition, in References]
STLCRef.store_lookup [definition, in References]
STLCRef.store_ty [definition, in References]
STLCRef.store_ty_lookup [definition, in References]
STLCRef.store_weakening [lemma, in References]
STLCRef.store_well_typed [definition, in References]
STLCRef.store_well_typed_snoc [lemma, in References]
STLCRef.ST_AppAbs [constructor, in References]
STLCRef.ST_App1 [constructor, in References]
STLCRef.ST_App2 [constructor, in References]
STLCRef.ST_Assign [constructor, in References]
STLCRef.ST_Assign1 [constructor, in References]
STLCRef.ST_Assign2 [constructor, in References]
STLCRef.ST_Deref [constructor, in References]
STLCRef.ST_DerefLoc [constructor, in References]
STLCRef.ST_If0 [constructor, in References]
STLCRef.ST_If0_Nonzero [constructor, in References]
STLCRef.ST_If0_Zero [constructor, in References]
STLCRef.ST_MultNats [constructor, in References]
STLCRef.ST_Mult1 [constructor, in References]
STLCRef.ST_Mult2 [constructor, in References]
STLCRef.ST_Pred [constructor, in References]
STLCRef.ST_PredNat [constructor, in References]
STLCRef.ST_Ref [constructor, in References]
STLCRef.ST_RefValue [constructor, in References]
STLCRef.ST_Succ [constructor, in References]
STLCRef.ST_SuccNat [constructor, in References]
STLCRef.subst [definition, in References]
STLCRef.substitution_preserves_typing [lemma, in References]
STLCRef.tm [inductive, in References]
STLCRef.tm_abs [constructor, in References]
STLCRef.tm_app [constructor, in References]
STLCRef.tm_assign [constructor, in References]
STLCRef.tm_deref [constructor, in References]
STLCRef.tm_if0 [constructor, in References]
STLCRef.tm_loc [constructor, in References]
STLCRef.tm_mult [constructor, in References]
STLCRef.tm_nat [constructor, in References]
STLCRef.tm_pred [constructor, in References]
STLCRef.tm_ref [constructor, in References]
STLCRef.tm_seq [definition, in References]
STLCRef.tm_succ [constructor, in References]
STLCRef.tm_unit [constructor, in References]
STLCRef.tm_var [constructor, in References]
STLCRef.ty [inductive, in References]
STLCRef.ty_arrow [constructor, in References]
STLCRef.ty_Nat [constructor, in References]
STLCRef.ty_Ref [constructor, in References]
STLCRef.ty_Unit [constructor, in References]
STLCRef.T_Abs [constructor, in References]
STLCRef.T_App [constructor, in References]
STLCRef.T_Assign [constructor, in References]
STLCRef.T_Deref [constructor, in References]
STLCRef.T_If0 [constructor, in References]
STLCRef.T_Loc [constructor, in References]
STLCRef.T_Mult [constructor, in References]
STLCRef.T_Nat [constructor, in References]
STLCRef.T_Pred [constructor, in References]
STLCRef.T_Ref [constructor, in References]
STLCRef.T_Succ [constructor, in References]
STLCRef.T_Unit [constructor, in References]
STLCRef.T_Var [constructor, in References]
STLCRef.value [inductive, in References]
STLCRef.v_abs [constructor, in References]
STLCRef.v_loc [constructor, in References]
STLCRef.v_nat [constructor, in References]
STLCRef.v_unit [constructor, in References]
STLCRef.::x_'/'_x_'==>'_x_'/'_x [notation, in References]
STLCRef.::x_'/'_x_'==>*'_x_'/'_x [notation, in References]
STLC.a [abbreviation, in Stlc]
STLC.afi_abs [constructor, in Stlc]
STLC.afi_app1 [constructor, in Stlc]
STLC.afi_app2 [constructor, in Stlc]
STLC.afi_if1 [constructor, in Stlc]
STLC.afi_if2 [constructor, in Stlc]
STLC.afi_if3 [constructor, in Stlc]
STLC.afi_var [constructor, in Stlc]
STLC.appears_free_in [inductive, in Stlc]
STLC.b [abbreviation, in Stlc]
STLC.c [abbreviation, in Stlc]
STLC.closed [definition, in Stlc]
STLC.context [definition, in Stlc]
STLC.Context [module, in Stlc]
STLC.Context.empty [definition, in Stlc]
STLC.Context.extend [definition, in Stlc]
STLC.Context.extend_eq [lemma, in Stlc]
STLC.Context.extend_neq [lemma, in Stlc]
STLC.Context.partial_map [definition, in Stlc]
STLC.context_invariance [lemma, in Stlc]
STLC.free_in_context [lemma, in Stlc]
STLC.has_type [inductive, in Stlc]
STLC.idB [abbreviation, in Stlc]
STLC.idBB [abbreviation, in Stlc]
STLC.idBBBB [abbreviation, in Stlc]
STLC.k [abbreviation, in Stlc]
STLC.preservation [lemma, in Stlc]
STLC.progress [lemma, in Stlc]
STLC.progress' [lemma, in Stlc]
STLC.step [inductive, in Stlc]
STLC.stepmany [abbreviation, in Stlc]
STLC.step_example1 [lemma, in Stlc]
STLC.step_example1' [lemma, in Stlc]
STLC.step_example2 [lemma, in Stlc]
STLC.step_example2' [lemma, in Stlc]
STLC.step_example3 [lemma, in Stlc]
STLC.ST_AppAbs [constructor, in Stlc]
STLC.ST_App1 [constructor, in Stlc]
STLC.ST_App2 [constructor, in Stlc]
STLC.ST_If [constructor, in Stlc]
STLC.ST_IfFalse [constructor, in Stlc]
STLC.ST_IfTrue [constructor, in Stlc]
STLC.subst [definition, in Stlc]
STLC.substitution_preserves_typing [lemma, in Stlc]
STLC.tm [inductive, in Stlc]
STLC.tm_abs [constructor, in Stlc]
STLC.tm_app [constructor, in Stlc]
STLC.tm_false [constructor, in Stlc]
STLC.tm_if [constructor, in Stlc]
STLC.tm_true [constructor, in Stlc]
STLC.tm_var [constructor, in Stlc]
STLC.ty [inductive, in Stlc]
STLC.typable_empty__closed [lemma, in Stlc]
STLC.typing_example_1 [definition, in Stlc]
STLC.typing_example_1' [definition, in Stlc]
STLC.typing_example_2 [definition, in Stlc]
STLC.typing_example_2_full [definition, in Stlc]
STLC.typing_example_3 [definition, in Stlc]
STLC.typing_nonexample_1 [definition, in Stlc]
STLC.typing_nonexample_3 [definition, in Stlc]
STLC.ty_arrow [constructor, in Stlc]
STLC.ty_Bool [constructor, in Stlc]
STLC.T_Abs [constructor, in Stlc]
STLC.T_App [constructor, in Stlc]
STLC.T_False [constructor, in Stlc]
STLC.t_false [constructor, in Stlc]
STLC.T_If [constructor, in Stlc]
STLC.t_true [constructor, in Stlc]
STLC.T_True [constructor, in Stlc]
STLC.T_Var [constructor, in Stlc]
STLC.value [inductive, in Stlc]
STLC.v_abs [constructor, in Stlc]
STLC.::x_'==>'_x [notation, in Stlc]
STLC.::x_'==>*'_x [notation, in Stlc]
strange_prop1 [definition, in Prop]
strange_prop2 [definition, in Prop]
string_of_list [definition, in ImpParser]
strong_progress [lemma, in Smallstep]
stuck [definition, in Types]
ST_AppAbs [constructor, in Norm]
ST_AppAbs [constructor, in Subtyping]
ST_AppAbs [constructor, in RecordSub]
ST_App1 [constructor, in Subtyping]
ST_App1 [constructor, in Norm]
ST_App1 [constructor, in RecordSub]
ST_App2 [constructor, in Norm]
ST_App2 [constructor, in Subtyping]
ST_App2 [constructor, in RecordSub]
ST_Fst [constructor, in Norm]
ST_FstPair [constructor, in Norm]
ST_If [constructor, in Subtyping]
ST_If [constructor, in Norm]
ST_If [constructor, in Types]
ST_IfFalse [constructor, in Types]
ST_IfFalse [constructor, in Norm]
ST_IfFalse [constructor, in Subtyping]
ST_IfTrue [constructor, in Subtyping]
ST_IfTrue [constructor, in Norm]
ST_IfTrue [constructor, in Types]
ST_Iszero [constructor, in Types]
ST_IszeroSucc [constructor, in Types]
ST_IszeroZero [constructor, in Types]
ST_Pair1 [constructor, in Norm]
ST_Pair2 [constructor, in Norm]
ST_PlusConstConst [constructor, in Smallstep]
ST_Plus1 [constructor, in Smallstep]
ST_Plus2 [constructor, in Smallstep]
ST_Pred [constructor, in Types]
ST_PredSucc [constructor, in Types]
ST_PredZero [constructor, in Types]
ST_ProjRcd [constructor, in RecordSub]
ST_Proj1 [constructor, in RecordSub]
ST_Rcd_Head [constructor, in RecordSub]
ST_Rcd_Tail [constructor, in RecordSub]
ST_Snd [constructor, in Norm]
ST_SndPair [constructor, in Norm]
ST_Succ [constructor, in Types]
subst [definition, in Subtyping]
subst [definition, in RecordSub]
subst [definition, in Norm]
substitution_preserves_typing [lemma, in Subtyping]
substitution_preserves_typing [lemma, in Norm]
substitution_preserves_typing [lemma, in RecordSub]
subst_aexp [definition, in Equiv]
subst_aexp_ex [definition, in Equiv]
subst_closed [lemma, in Norm]
subst_equiv_property [definition, in Equiv]
subst_inequiv [lemma, in Equiv]
subst_msubst [lemma, in Norm]
subst_not_afi [lemma, in Norm]
subtract_slowly [definition, in Imp]
subtract_slowly [definition, in Hoare]
subtract_slowly_body [definition, in Imp]
subtract_slowly_correct [lemma, in Hoare]
subtract_slowly_dec [definition, in Hoare]
subtract_slowly_dec_correct [lemma, in Hoare]
subtract_slowly_invariant [definition, in Hoare]
subtract_3_from_5_slowly [definition, in Imp]
subtype [axiom, in UseAuto]
subtype [inductive, in RecordSub]
subtype [inductive, in Subtyping]
subtype_refl [axiom, in UseAuto]
subtype_trans [axiom, in UseAuto]
subtype__wf [lemma, in RecordSub]
Subtyping [library]
SubtypingInversion [module, in UseAuto]
SubtypingInversion.abs_arrow [lemma, in UseAuto]
SubtypingInversion.abs_arrow' [lemma, in UseAuto]
SubtypingInversion.substitution_preserves_typing [lemma, in UseAuto]
sub_inversion_arrow [lemma, in RecordSub]
sub_inversion_arrow [lemma, in Subtyping]
sub_inversion_Bool [lemma, in Subtyping]
succ_hastype_nat__hastype_nat [definition, in Types]
sum [definition, in Hoare]
sum_program [definition, in Hoare]
sum_program_spec [definition, in Hoare]
sunday [constructor, in Basics]
swap_if_branches [lemma, in Equiv]
swap_noninterfering_assignments [lemma, in Equiv]
swap_subst [lemma, in Norm]
Symbols [library]
symmetric [definition, in Rel]
sym_aequiv [lemma, in Equiv]
sym_bequiv [lemma, in Equiv]
sym_cequiv [lemma, in Equiv]
S_Arrow [constructor, in RecordSub]
S_Arrow [constructor, in Subtyping]
s_compile [definition, in Imp]
s_compile_correct [lemma, in Imp]
s_execute [definition, in Imp]
s_execute1 [definition, in Imp]
s_execute2 [definition, in Imp]
S_inj [lemma, in Poly]
S_nbeq_0 [lemma, in Basics]
S_RcdDepth [constructor, in RecordSub]
S_RcdPerm [constructor, in RecordSub]
S_RcdWidth [constructor, in RecordSub]
S_Refl [constructor, in RecordSub]
S_Refl [constructor, in Subtyping]
S_Top [constructor, in RecordSub]
S_Top [constructor, in Subtyping]
S_Trans [constructor, in RecordSub]
S_Trans [constructor, in Subtyping]
T
tail [definition, in ImpList]tass [definition, in Norm]
teen [definition, in Prop]
Temp1 [module, in Smallstep]
Temp1.step [inductive, in Smallstep]
Temp1.ST_PlusConstConst [constructor, in Smallstep]
Temp1.ST_Plus1 [constructor, in Smallstep]
Temp1.ST_Plus2 [constructor, in Smallstep]
Temp1.value [inductive, in Smallstep]
Temp1.value_not_same_as_normal_form [lemma, in Smallstep]
Temp1.v_const [constructor, in Smallstep]
Temp1.v_funny [constructor, in Smallstep]
Temp1.::x_'==>'_x [notation, in Smallstep]
Temp2 [module, in Smallstep]
Temp2.step [inductive, in Smallstep]
Temp2.ST_Funny [constructor, in Smallstep]
Temp2.ST_PlusConstConst [constructor, in Smallstep]
Temp2.ST_Plus1 [constructor, in Smallstep]
Temp2.ST_Plus2 [constructor, in Smallstep]
Temp2.value [inductive, in Smallstep]
Temp2.value_not_same_as_normal_form [lemma, in Smallstep]
Temp2.v_const [constructor, in Smallstep]
Temp2.::x_'==>'_x [notation, in Smallstep]
Temp3 [module, in Smallstep]
Temp3.step [inductive, in Smallstep]
Temp3.ST_PlusConstConst [constructor, in Smallstep]
Temp3.ST_Plus1 [constructor, in Smallstep]
Temp3.value [inductive, in Smallstep]
Temp3.value_not_same_as_normal_form [lemma, in Smallstep]
Temp3.v_const [constructor, in Smallstep]
Temp3.::x_'==>'_x [notation, in Smallstep]
Temp4 [module, in Smallstep]
Temp4.bool_step_prop1 [definition, in Smallstep]
Temp4.bool_step_prop2 [definition, in Smallstep]
Temp4.bool_step_prop3 [definition, in Smallstep]
Temp4.step [inductive, in Smallstep]
Temp4.step_deterministic [lemma, in Smallstep]
Temp4.strong_progress [lemma, in Smallstep]
Temp4.ST_If [constructor, in Smallstep]
Temp4.ST_IfFalse [constructor, in Smallstep]
Temp4.ST_IfTrue [constructor, in Smallstep]
Temp4.Temp5 [module, in Smallstep]
Temp4.Temp5.bool_step_prop4 [definition, in Smallstep]
Temp4.Temp5.bool_step_prop4_holds [definition, in Smallstep]
Temp4.Temp5.step [inductive, in Smallstep]
Temp4.Temp5.ST_If [constructor, in Smallstep]
Temp4.Temp5.ST_IfFalse [constructor, in Smallstep]
Temp4.Temp5.ST_IfTrue [constructor, in Smallstep]
Temp4.Temp5.::x_'==>'_x [notation, in Smallstep]
Temp4.tm [inductive, in Smallstep]
Temp4.tm_false [constructor, in Smallstep]
Temp4.tm_if [constructor, in Smallstep]
Temp4.tm_true [constructor, in Smallstep]
Temp4.value [inductive, in Smallstep]
Temp4.v_false [constructor, in Smallstep]
Temp4.v_true [constructor, in Smallstep]
Temp4.::x_'==>'_x [notation, in Smallstep]
test_andb31 [definition, in Basics]
test_andb32 [definition, in Basics]
test_andb33 [definition, in Basics]
test_andb34 [definition, in Basics]
test_anon_fun' [definition, in Poly]
test_ble_nat1 [definition, in Basics]
test_ble_nat2 [definition, in Basics]
test_ble_nat3 [definition, in Basics]
test_blt_nat1 [definition, in Basics]
test_blt_nat2 [definition, in Basics]
test_blt_nat3 [definition, in Basics]
test_ceval [definition, in Imp]
test_countoddmembers'1 [definition, in Poly]
test_countoddmembers'2 [definition, in Poly]
test_countoddmembers'3 [definition, in Poly]
test_doit3times [definition, in Poly]
test_doit3times' [definition, in Poly]
test_factorial1 [definition, in Basics]
test_factorial2 [definition, in Basics]
test_filter1 [definition, in Poly]
test_filter2 [definition, in Poly]
test_filter2' [definition, in Poly]
test_filter_even_gt7_1 [definition, in Poly]
test_filter_even_gt7_2 [definition, in Poly]
test_flat_map1 [definition, in Poly]
test_fold_length1 [definition, in Poly]
test_hd_opt1 [definition, in Poly]
test_hd_opt2 [definition, in Poly]
test_index1 [definition, in Poly]
test_index2 [definition, in Poly]
test_index3 [definition, in Poly]
test_length1 [definition, in Poly]
test_length2 [definition, in Poly]
test_le1 [lemma, in Logic]
test_le2 [lemma, in Logic]
test_le3 [lemma, in Logic]
test_map1 [definition, in Poly]
test_map2 [definition, in Poly]
test_map3 [definition, in Poly]
test_mult1 [definition, in Basics]
test_nandb1 [definition, in Basics]
test_nandb2 [definition, in Basics]
test_nandb3 [definition, in Basics]
test_nandb4 [definition, in Basics]
test_next_weekday [definition, in Basics]
test_nostutter_1 [definition, in Logic]
test_nostutter_2 [definition, in Logic]
test_nostutter_3 [definition, in Logic]
test_nostutter_4 [definition, in Logic]
test_oddb1 [definition, in Basics]
test_oddb2 [definition, in Basics]
test_orb1 [definition, in Basics]
test_orb2 [definition, in Basics]
test_orb3 [definition, in Basics]
test_orb4 [definition, in Basics]
test_partition1 [definition, in Poly]
test_partition2 [definition, in Poly]
test_pe_aexp1 [definition, in PE]
test_pe_bexp1 [definition, in PE]
test_pe_bexp2 [definition, in PE]
test_pe_override [definition, in PE]
test_plus3 [definition, in Poly]
test_plus3' [definition, in Poly]
test_plus3'' [definition, in Poly]
test_repeat1 [definition, in Poly]
test_rev1 [definition, in Poly]
test_rev2 [definition, in Poly]
test_stepmany_1 [lemma, in Smallstep]
test_stepmany_1' [lemma, in Smallstep]
test_stepmany_2 [lemma, in Smallstep]
test_stepmany_3 [lemma, in Smallstep]
test_stepmany_4 [lemma, in Smallstep]
text_pe_aexp2 [definition, in PE]
thursday [constructor, in Basics]
tm [inductive, in Norm]
tm [inductive, in Smallstep]
tm [inductive, in RecordSub]
tm [inductive, in Types]
tm [inductive, in Subtyping]
tm_abs [constructor, in Norm]
tm_abs [constructor, in Subtyping]
tm_abs [constructor, in RecordSub]
tm_app [constructor, in Norm]
tm_app [constructor, in Subtyping]
tm_app [constructor, in RecordSub]
tm_const [constructor, in Smallstep]
tm_false [constructor, in Norm]
tm_false [constructor, in Subtyping]
tm_false [constructor, in Types]
tm_fst [constructor, in Norm]
tm_if [constructor, in Norm]
tm_if [constructor, in Subtyping]
tm_if [constructor, in Types]
tm_iszero [constructor, in Types]
tm_lookup [definition, in RecordSub]
tm_pair [constructor, in Norm]
tm_plus [constructor, in Smallstep]
tm_pred [constructor, in Types]
tm_proj [constructor, in RecordSub]
tm_rcons [constructor, in RecordSub]
tm_rnil [constructor, in RecordSub]
tm_snd [constructor, in Norm]
tm_succ [constructor, in Types]
tm_true [constructor, in Subtyping]
tm_true [constructor, in Norm]
tm_true [constructor, in Types]
tm_unit [constructor, in Subtyping]
tm_var [constructor, in Norm]
tm_var [constructor, in Subtyping]
tm_var [constructor, in RecordSub]
tm_zero [constructor, in Types]
token [definition, in ImpParser]
tokenize [definition, in ImpParser]
tokenize_ex1 [definition, in ImpParser]
tokenize_helper [definition, in ImpParser]
tot [constructor, in SfLib]
total_relation [inductive, in SfLib]
transitive [definition, in Rel]
transitivity_bad_hint_1 [lemma, in UseAuto]
transitivity_workaround_1 [lemma, in UseAuto]
transitivity_workaround_2 [lemma, in UseAuto]
trans_aequiv [lemma, in Equiv]
trans_bequiv [lemma, in Equiv]
trans_cequiv [lemma, in Equiv]
trans_eq [lemma, in Poly]
trans_eq_example [definition, in Poly]
trans_eq_example' [definition, in Poly]
trans_eq_exercise [definition, in Poly]
tree [inductive, in Prop]
true [constructor, in Basics]
true_for_all_numbers [definition, in Prop]
true_for_n__true_for_Sn [definition, in Prop]
true_for_zero [definition, in Prop]
tuesday [constructor, in Basics]
ty [inductive, in Subtyping]
ty [inductive, in RecordSub]
ty [inductive, in Norm]
ty [inductive, in Types]
typ [axiom, in UseAuto]
typable_empty__closed [lemma, in Norm]
Typechecking [library]
Types [library]
typing_inversion_abs [lemma, in RecordSub]
typing_inversion_abs [lemma, in Subtyping]
typing_inversion_app [lemma, in RecordSub]
typing_inversion_app [lemma, in Subtyping]
typing_inversion_false [lemma, in Subtyping]
typing_inversion_if [lemma, in Subtyping]
typing_inversion_proj [lemma, in RecordSub]
typing_inversion_rcons [lemma, in RecordSub]
typing_inversion_true [lemma, in Subtyping]
typing_inversion_unit [lemma, in Subtyping]
typing_inversion_var [lemma, in RecordSub]
typing_inversion_var [lemma, in Subtyping]
ty_arrow [constructor, in RecordSub]
ty_arrow [constructor, in Subtyping]
ty_arrow [constructor, in Norm]
ty_base [constructor, in RecordSub]
ty_base [constructor, in Subtyping]
ty_Bool [constructor, in Types]
ty_Bool [constructor, in Norm]
ty_Bool [constructor, in Subtyping]
ty_lookup [definition, in RecordSub]
ty_Nat [constructor, in Types]
ty_prod [constructor, in Norm]
ty_rcons [constructor, in RecordSub]
ty_rnil [constructor, in RecordSub]
ty_Top [constructor, in Subtyping]
ty_Top [constructor, in RecordSub]
ty_Unit [constructor, in Subtyping]
T_Abs [constructor, in Norm]
T_Abs [constructor, in Subtyping]
T_Abs [constructor, in RecordSub]
T_App [constructor, in Subtyping]
T_App [constructor, in RecordSub]
T_App [constructor, in Norm]
T_False [constructor, in Types]
t_false [constructor, in Subtyping]
T_False [constructor, in Norm]
T_False [constructor, in Subtyping]
T_Fst [constructor, in Norm]
T_If [constructor, in Norm]
T_If [constructor, in Types]
T_If [constructor, in Subtyping]
T_Iszero [constructor, in Types]
T_Pair [constructor, in Norm]
T_Pred [constructor, in Types]
T_Proj [constructor, in RecordSub]
T_RCons [constructor, in RecordSub]
T_RNil [constructor, in RecordSub]
T_Snd [constructor, in Norm]
T_Sub [constructor, in RecordSub]
T_Sub [constructor, in Subtyping]
T_Succ [constructor, in Types]
t_true [constructor, in Subtyping]
T_True [constructor, in Types]
T_True [constructor, in Norm]
T_True [constructor, in Subtyping]
T_Unit [constructor, in Subtyping]
T_Var [constructor, in Norm]
T_Var [constructor, in RecordSub]
T_Var [constructor, in Subtyping]
T_Zero [constructor, in Types]
U
uncurry_curry [lemma, in Poly]UnfoldsExample [module, in UseTactics]
UnfoldsExample.bexp_eval_true [lemma, in UseTactics]
unfold_example [lemma, in Poly]
unfold_example_bad [lemma, in Poly]
update [definition, in Imp]
update [definition, in ImpList]
update_eq [lemma, in ImpList]
update_eq [lemma, in Imp]
update_example [lemma, in Imp]
update_neq [lemma, in ImpList]
update_neq [lemma, in Imp]
update_permute [lemma, in Imp]
update_permute [lemma, in ImpList]
update_same [lemma, in Imp]
update_same [lemma, in ImpList]
update_shadow [lemma, in Imp]
update_shadow [lemma, in ImpList]
UseAuto [library]
UseTactics [library]
V
vacuous_substitution [lemma, in Norm]val [inductive, in ImpList]
value [inductive, in Smallstep]
value [inductive, in RecordSub]
value [inductive, in Norm]
value [inductive, in Subtyping]
value [definition, in Types]
value_halts [lemma, in Norm]
value_is_nf [lemma, in Smallstep]
value_is_nf [lemma, in Types]
value__normal [lemma, in Norm]
var_not_used_in_aexp [inductive, in Equiv]
verification_conditions [definition, in Hoare]
verification_correct [lemma, in Hoare]
VList [constructor, in ImpList]
VNat [constructor, in ImpList]
VNUId [constructor, in Equiv]
VNUMinus [constructor, in Equiv]
VNUMult [constructor, in Equiv]
VNUNum [constructor, in Equiv]
VNUPlus [constructor, in Equiv]
v_abs [constructor, in RecordSub]
v_abs [constructor, in Norm]
v_abs [constructor, in Subtyping]
V_cons [constructor, in Norm]
v_const [constructor, in Smallstep]
v_false [constructor, in Norm]
V_nil [constructor, in Norm]
v_pair [constructor, in Norm]
v_rcons [constructor, in RecordSub]
v_rnil [constructor, in RecordSub]
v_true [constructor, in Norm]
v_unit [constructor, in Subtyping]
W
wednesday [constructor, in Basics]well_formed_ty [inductive, in RecordSub]
wfty_arrow [constructor, in RecordSub]
wfty_base [constructor, in RecordSub]
wfty_rcons [constructor, in RecordSub]
wfty_rnil [constructor, in RecordSub]
wfty_Top [constructor, in RecordSub]
wf_rcd_lookup [lemma, in RecordSub]
while_example [definition, in Hoare]
WHILE_false [lemma, in Equiv]
WHILE_true [lemma, in Equiv]
WHILE_true_nonterm [lemma, in Equiv]
white [constructor, in ImpParser]
working_of_auto_1 [lemma, in UseAuto]
working_of_auto_2 [lemma, in UseAuto]
X
X [definition, in ImpList]X [definition, in Imp]
XtimesYinZ [definition, in Imp]
Y
Y [definition, in ImpList]Y [definition, in Imp]
yes [constructor, in Prop]
yesno [inductive, in Prop]
Z
Z [definition, in ImpList]Z [definition, in Imp]
zero_nbeq_plus_1 [lemma, in Basics]
zero_nbeq_S [lemma, in Basics]
:
:dcom_scope:x_'::='_x_'{{'_x_'}}' [notation, in Hoare]:dcom_scope:x_';'_x [notation, in Hoare]
:dcom_scope:x_'=>'_'{{'_x_'}}' [notation, in Hoare]
:dcom_scope:'IFB'_x_'THEN'_'{{'_x_'}}'_x_'ELSE'_'{{'_x_'}}'_x_'FI' [notation, in Hoare]
:dcom_scope:'SKIP'_'{{'_x_'}}' [notation, in Hoare]
:dcom_scope:'WHILE'_x_'DO'_'{{'_x_'}}'_x_'END'_'{{'_x_'}}' [notation, in Hoare]
:dcom_scope:'=>'_'{{'_x_'}}'_x [notation, in Hoare]
:dcom_scope:'{{'_x_'}}'_x [notation, in Hoare]
:hoare_spec_scope:'{{'_x_'}}'_x [notation, in Hoare]
:hoare_spec_scope:'{{'_x_'}}'_x_'{{'_x_'}}' [notation, in Hoare]
:ltac_scope:'>>' [notation, in LibTactics]
:ltac_scope:'>>'_x [notation, in LibTactics]
:ltac_scope:'>>'_x_x [notation, in LibTactics]
:ltac_scope:'>>'_x_x_x [notation, in LibTactics]
:ltac_scope:'>>'_x_x_x_x [notation, in LibTactics]
:ltac_scope:'>>'_x_x_x_x_x [notation, in LibTactics]
:ltac_scope:'>>'_x_x_x_x_x_x [notation, in LibTactics]
:ltac_scope:'>>'_x_x_x_x_x_x_x [notation, in LibTactics]
:ltac_scope:'>>'_x_x_x_x_x_x_x_x [notation, in LibTactics]
:ltac_scope:'>>'_x_x_x_x_x_x_x_x_x [notation, in LibTactics]
:ltac_scope:'>>'_x_x_x_x_x_x_x_x_x_x [notation, in LibTactics]
:ltac_scope:'>>'_x_x_x_x_x_x_x_x_x_x_x [notation, in LibTactics]
:ltac_scope:'>>'_x_x_x_x_x_x_x_x_x_x_x_x [notation, in LibTactics]
:ltac_scope:'>>'_x_x_x_x_x_x_x_x_x_x_x_x_x [notation, in LibTactics]
:ltac_scope:'__' [notation, in LibTactics]
:ltac_scope:'___' [notation, in LibTactics]
:nat_scope:x_'*'_x [notation, in Basics]
:nat_scope:x_'+'_x [notation, in Basics]
:nat_scope:x_'-'_x [notation, in Basics]
:nat_scope:x_'<=?'_x [notation, in ImpParser]
:type_scope:x_'*'_x [notation, in Poly]
:type_scope:x_'/\'_x [notation, in Logic]
:type_scope:x_'<->'_x [notation, in Logic]
:type_scope:x_'<>'_x [notation, in Logic]
:type_scope:x_'\/'_x [notation, in Logic]
:type_scope:'exists'_x_x_x_x_x_x_x_x_x_x_','_x [notation, in LibTactics]
:type_scope:'exists'_x_x_x_x_x_x_x_x_x_','_x [notation, in LibTactics]
:type_scope:'exists'_x_x_x_x_x_x_x_x_','_x [notation, in LibTactics]
:type_scope:'exists'_x_x_x_x_x_x_x_','_x [notation, in LibTactics]
:type_scope:'exists'_x_x_x_x_x_x_','_x [notation, in LibTactics]
:type_scope:'exists'_x_x_x_x_x_','_x [notation, in LibTactics]
:type_scope:'exists'_x_x_x_x_','_x [notation, in LibTactics]
:type_scope:'exists'_x_x_x_','_x [notation, in LibTactics]
:type_scope:'exists'_x_x_','_x [notation, in LibTactics]
:type_scope:'exists'_x_','_x [notation, in Logic]
:type_scope:'exists'_x_','_x [notation, in LibTactics]
:type_scope:'exists'_x_':'_x_','_x [notation, in Logic]
:type_scope:'~'_x [notation, in Logic]
::x_'++'_x [notation, in SfLib]
::x_'++'_x [notation, in Poly]
::x_'/'_x_'/'_x_'||'_x [notation, in PE]
::x_'/'_x_'==>a'_x [notation, in Smallstep]
::x_'/'_x_'==>a*'_x [notation, in Types]
::x_'/'_x_'==>b'_x [notation, in Smallstep]
::x_'/'_x_'==>'_x_'/'_x [notation, in Smallstep]
::x_'/'_x_'||'''_x [notation, in Equiv]
::x_'/'_x_'||'_x [notation, in Imp]
::x_'/'_x_'||'_x [notation, in ImpList]
::x_'/'_x_'||'_x_'/'_x [notation, in PE]
::x_'::'_x [notation, in Poly]
::x_'::='_x [notation, in Imp]
::x_'::='_x [notation, in ImpList]
::x_';'_x [notation, in Imp]
::x_';'_x [notation, in ImpList]
::x_'<'_x [notation, in Logic]
::x_'<='_x [notation, in Logic]
::x_'<~~>'_x [notation, in Hoare]
::x_'='''_x [notation, in LibTactics]
::x_'==>'_x [notation, in Types]
::x_'==>'_x [notation, in Norm]
::x_'==>'_x [notation, in Subtyping]
::x_'==>'_x [notation, in RecordSub]
::x_'==>'_x [notation, in Smallstep]
::x_'==>*'_x [notation, in Smallstep]
::x_'==>*'_x [notation, in Types]
::x_'==>*'_x [notation, in Norm]
::x_'||'_x [notation, in Smallstep]
::x_'~'_x [notation, in Equiv]
::x_'~~>'_x [notation, in Hoare]
::'DO'_'('_x_','_x_')'_'<--'_x_';;'_x_'OR'_x [notation, in ImpParser]
::'DO'_'('_x_','_x_')'_'<=='_x_';;'_x [notation, in ImpParser]
::'IFB'_x_'THEN'_x_'ELSE'_x_'FI' [notation, in Imp]
::'IFB'_x_'THEN'_x_'ELSE'_x_'FI' [notation, in ImpList]
::'LETOPT'_x_'<=='_x_'IN'_x [notation, in Imp]
::'nosimpl'_x [notation, in LibTactics]
::'Register'_x_x [notation, in LibTactics]
::'SKIP' [notation, in ImpList]
::'SKIP' [notation, in Imp]
::'Something' [notation, in LibTactics]
::'WHILE'_x_'DO'_x_'END' [notation, in Imp]
::'WHILE'_x_'DO'_x_'END' [notation, in ImpList]
::'('_x_','_x_')' [notation, in Poly]
::'['_x_','_'..'_','_x_']' [notation, in Poly]
::'['_x_','_'..'_','_x_']' [notation, in SfLib]
::'['_']' [notation, in Poly]
::'['_']' [notation, in SfLib]
Lemma Index
A
abs_arrow [in Subtyping]abs_arrow [in RecordSub]
aequiv_example [in Equiv]
aeval_weakening [in Equiv]
AExp.aeval_iff_aevalR [in Imp]
AExp.aeval_iff_aevalR' [in Imp]
AExp.foo [in Imp]
AExp.foo' [in Imp]
AExp.optimize_0plus_sound [in Imp]
AExp.optimize_0plus_sound' [in Imp]
AExp.optimize_0plus_sound'' [in Imp]
AExp.optimize_0plus_sound''' [in Imp]
all3_spec [in Basics]
always_loop_hoare [in Hoare]
always_loop_hoare' [in Hoare]
andb_false [in Logic]
andb_false_r [in Basics]
andb_true [in SfLib]
andb_true_elim1 [in SfLib]
andb_true_elim1 [in Basics]
andb_true_elim2 [in SfLib]
andb_true_elim2 [in Basics]
andb_true__and [in Logic]
and_assoc [in Logic]
and_commut [in Logic]
and_example [in Logic]
and_example' [in Logic]
and__andb_true [in Logic]
appears_in_app [in Logic]
appears_in_app_split [in Logic]
appears_in_snoc1 [in Hoare]
appears_in_snoc2 [in Hoare]
appears_in_snoc3 [in Hoare]
append_nil [in Hoare]
append_singleton_equation [in Hoare]
app_appears_in [in Logic]
app_ass' [in Poly]
app_length [in Logic]
app_length_cons [in Gen]
app_length_twice [in Gen]
assign_aequiv [in Equiv]
assign_removes [in PE]
auto_example_1 [in Types]
auto_example_2 [in Types]
auto_example_2a [in Types]
B
bequiv_example [in Equiv]beq_false_not_eq [in Logic]
beq_id_eq [in SfLib]
beq_id_eq [in ImpList]
beq_id_false_not_eq [in SfLib]
beq_id_false_not_eq [in ImpList]
beq_id_refl [in ImpList]
beq_id_refl [in SfLib]
beq_id_sym [in SfLib]
beq_nat_eq [in Poly]
beq_nat_eq' [in Poly]
beq_nat_refl [in Basics]
beq_nat_refl [in Hoare]
beq_nat_sym [in Poly]
beq_nat_sym [in SfLib]
beq_nat_trans [in Poly]
beq_nat_0_l [in Poly]
beq_nat_0_r [in Poly]
beq_true__eq [in Hoare]
bexp_eval_false [in Hoare]
bexp_eval_true [in Hoare]
ble_nat_false [in Logic]
ble_nat_false [in SfLib]
ble_nat_n_Sn_false [in Logic]
ble_nat_refl [in Basics]
ble_nat_true [in SfLib]
ble_nat_true [in Logic]
C
canonical_forms_of_arrow_types [in RecordSub]canonical_forms_of_arrow_types [in Subtyping]
canonical_forms_of_Bool [in Subtyping]
CasesExample.update_same [in UseTactics]
CasesExample.update_same' [in UseTactics]
CAss_congruence [in Equiv]
cequiv__cequiv' [in Equiv]
ceval_and_ceval_step_coincide [in Imp]
ceval_deterministic [in Imp]
ceval_deterministic' [in Imp]
ceval_extensionality [in PE]
ceval_step_more [in Imp]
ceval_step__ceval [in Imp]
ceval__ceval_step [in Imp]
CIf_congruence [in Equiv]
CImp.par_body_n [in Smallstep]
CImp.par_body_n__Sn [in Smallstep]
CImp.par_loop_any_X [in Smallstep]
classic_double_neg [in Logic]
congruence_demo_1 [in UseAuto]
congruence_demo_2 [in UseAuto]
congruence_demo_3 [in UseAuto]
congruence_demo_4 [in UseAuto]
context_invariance [in Norm]
context_invariance [in RecordSub]
context_invariance [in Subtyping]
contradiction_implies_anything [in Logic]
contrapositive [in Logic]
CSeq_congruence [in Equiv]
curry_uncurry [in Poly]
CWhile_congruence [in Equiv]
D
dec_while_correct [in Hoare]demo_auto_absurd_1 [in UseAuto]
demo_auto_absurd_2 [in UseAuto]
demo_false [in UseAuto]
demo_false [in UseTactics]
demo_false_arg [in UseTactics]
demo_hint_unfold_context_1 [in UseAuto]
demo_hint_unfold_context_2 [in UseAuto]
demo_hint_unfold_goal_1 [in UseAuto]
demo_hint_unfold_goal_2 [in UseAuto]
demo_tryfalse [in UseTactics]
DeterministicImp.ceval_deterministic [in UseAuto]
DeterministicImp.ceval_deterministic' [in UseAuto]
DeterministicImp.ceval_deterministic'' [in UseAuto]
DeterministicImp.ceval_deterministic''' [in UseAuto]
DeterministicImp.ceval_deterministic'''' [in UseAuto]
dist_exists_or [in Logic]
dist_not_exists [in Logic]
double_even [in Prop]
double_injective [in Poly]
double_injective' [in Gen]
double_injective_FAILED [in Gen]
double_injective_take2 [in Gen]
double_injective_take2_FAILED [in Gen]
double_neg [in Logic]
double_plus [in Basics]
duplicate_subst [in Norm]
dup_lemma [in LibTactics]
E
EqualityExamples.demo_applys_eq_1 [in UseTactics]EqualityExamples.demo_applys_eq_2 [in UseTactics]
EqualityExamples.demo_applys_eq_3 [in UseTactics]
EqualityExamples.demo_fequals [in UseTactics]
EqualityExamples.demo_substs [in UseTactics]
EqualityExamples.mult_0_plus [in UseTactics]
EqualityExamples.mult_0_plus' [in UseTactics]
EqualityExamples.mult_0_plus'' [in UseTactics]
equality_by_auto [in UseAuto]
equates_0 [in LibTactics]
equates_1 [in LibTactics]
equates_2 [in LibTactics]
equates_3 [in LibTactics]
equates_4 [in LibTactics]
equates_5 [in LibTactics]
equates_6 [in LibTactics]
eq_add_S [in Poly]
eq_remove_S [in Poly]
eval_assign [in PE]
eval__stepmany [in Smallstep]
eval__value [in Smallstep]
evenb_n__oddb_Sn [in Basics]
even5_nonsense [in Prop]
even_ev [in Logic]
even_ev' [in Logic]
ev_even [in Prop]
ev_even' [in Prop]
ev_ev_even [in Prop]
ev_minus2 [in Prop]
ev_minus2' [in Prop]
ev_MyProp [in Prop]
ev_MyProp' [in Prop]
ev_not_ev_S [in SfLib]
ev_not_ev_S [in Logic]
ev_plus4' [in Prop]
ev_plus_plus [in Prop]
ev_sum [in Prop]
ExamplesInstantiations.substitution_preserves_typing [in UseTactics]
ExamplesLets.demo_lets_underscore [in UseTactics]
ExamplesLets.demo_lets_1 [in UseTactics]
ExamplesLets.demo_lets_2 [in UseTactics]
ExamplesLets.demo_lets_3 [in UseTactics]
ExamplesLets.demo_lets_4 [in UseTactics]
ExamplesLets.demo_lets_5 [in UseTactics]
existsb_app [in PE]
existsb_beq_id_filter [in PE]
exists_example_2 [in Logic]
extend_eq [in SfLib]
extend_neq [in SfLib]
extend_shadow [in SfLib]
ex_falso_quodlibet [in Logic]
ex_falso_quodlibet [in SfLib]
F
Factorial.fact_com_correct [in Hoare]fact_body_preserves_invariant [in Imp]
fact_com_correct [in Imp]
fact_loop_preserves_invariant [in Imp]
False_and_P_imp [in HoareAsLogic]
False_implies_nonsense [in Logic]
fdfs_wed [in Prop]
filter_exercise [in Poly]
find_parity_correct [in Hoare]
five_not_even [in Logic]
fold_constants_aexp_sound [in Equiv]
fold_constants_bexp_sound [in Equiv]
fold_constants_com_sound [in Equiv]
fold_length_correct [in Poly]
four_ev' [in Prop]
free_in_context [in Subtyping]
free_in_context [in Norm]
free_in_context [in RecordSub]
G
gds [in Prop]GenExample.substitution_preserves_typing [in UseTactics]
guard_false_after_loop [in Imp]
H
has_type__wf [in RecordSub]hoare_asgn [in Hoare]
hoare_asgn_eq [in Hoare]
hoare_asgn_weakest [in Hoare]
hoare_consequence [in Hoare]
hoare_consequence_post [in Hoare]
hoare_consequence_pre [in Hoare]
hoare_if [in Hoare]
hoare_post_true [in Hoare]
hoare_pre_false [in Hoare]
hoare_proof_sound [in HoareAsLogic]
hoare_seq [in Hoare]
hoare_skip [in Hoare]
hoare_while [in Hoare]
H_Post_True_deriv [in HoareAsLogic]
H_Pre_False_deriv [in HoareAsLogic]
I
identity_assignment [in Equiv]identity_assignment_first_try [in Equiv]
Id.beq_id_eq [in Imp]
Id.beq_id_false_not_eq [in Imp]
Id.beq_id_refl [in Imp]
Id.beq_id_sym [in Imp]
Id.not_eq_beq_id_false [in Imp]
IFB_false [in Equiv]
IFB_true [in Equiv]
IFB_true_simple [in Equiv]
iff_implies [in Logic]
iff_intro_swap [in LibTactics]
iff_refl [in Logic]
iff_sym [in Logic]
iff_trans [in Logic]
iff_trans [in Equiv]
index_after_last [in Gen]
inequiv_exercise [in Equiv]
instantiation_domains_match [in Norm]
instantiation_drop [in Norm]
instantiation_env_closed [in Norm]
instantiation_R [in Norm]
IntrovExamples.ceval_and_ceval_step_coincide [in UseTactics]
IntrovExamples.ceval_deterministic [in UseTactics]
IntrovExamples.ceval_deterministic' [in UseTactics]
IntrovExamples.ceval_step__ceval [in UseTactics]
InvertsExamples.ceval_deterministic [in UseTactics]
InvertsExamples.ceval_deterministic' [in UseTactics]
InvertsExamples.skip_left [in UseTactics]
InvertsExamples.skip_left' [in UseTactics]
L
length_snoc' [in Poly]length_snoc''' [in Gen]
le_antisymmetric [in Rel]
le_not_a_partial_function [in Rel]
le_not_symmetric [in Rel]
le_order [in Rel]
le_plus_l [in Logic]
le_reflexive [in Rel]
le_Sn_le [in Rel]
le_Sn_n [in Rel]
le_step [in Rel]
le_S_n [in Rel]
le_trans [in Rel]
list_member_correct [in Hoare]
list_member_correct' [in Hoare]
lookup_field_in_value [in RecordSub]
Loop.ceval_count_complete [in PE]
Loop.ceval_count_sound [in PE]
Loop.pe_ceval_count_le [in PE]
Loop.pe_compare_nil_lookup [in PE]
Loop.pe_compare_nil_override [in PE]
Loop.pe_com_complete [in PE]
Loop.pe_com_correct [in PE]
Loop.pe_com_sound [in PE]
loop_never_stops [in Imp]
loop_never_stops [in ImpList]
loop_unrolling [in Equiv]
ltac_database_provide [in LibTactics]
ltac_something_eq [in LibTactics]
ltac_something_hide [in LibTactics]
ltac_something_show [in LibTactics]
lt_S [in Logic]
lt_trans [in Rel]
lt_trans' [in Rel]
lt_trans'' [in Rel]
M
map_rev [in Poly]mextend_drop [in Norm]
mextend_lookup [in Norm]
minus_diag [in Basics]
msubst_abs [in Norm]
msubst_app [in Norm]
msubst_closed [in Norm]
msubst_preserves_typing [in Norm]
msubst_R [in Norm]
msubst_var [in Norm]
mult_assoc [in Basics]
mult_comm [in Basics]
mult_plus_distr_r [in Basics]
mult_0_l [in Basics]
mult_0_plus [in Basics]
mult_0_plus' [in Basics]
mult_0_r [in Basics]
mult_0_r' [in Prop]
mult_0_r'' [in Prop]
mult_1_l [in Basics]
mult_1_plus [in Basics]
MyEquality.two_defs_of_eq_coincide [in Logic]
MyProp_ev [in Prop]
MyProp_plustwo [in Prop]
MyProp_ten [in Prop]
MyProp_0 [in Prop]
N
NaryExamples.demo_branch [in UseTactics]NaryExamples.demo_splits [in UseTactics]
NaryExamples.progress [in UseTactics]
NatList.app_ass [in Lists]
NatList.app_ass4 [in Lists]
NatList.app_length [in Lists]
NatList.app_nil_end [in Lists]
NatList.beq_natlist_refl [in Lists]
NatList.ble_n_Sn [in Lists]
NatList.count_member_nonzero [in Lists]
NatList.Dictionary.dictionary_invariant1 [in Lists]
NatList.Dictionary.dictionary_invariant2 [in Lists]
NatList.distr_rev [in Lists]
NatList.fst_swap_is_snd [in Lists]
NatList.length_snoc [in Lists]
NatList.nil_app [in Lists]
NatList.nonzeros_length [in Lists]
NatList.option_elim_hd [in Lists]
NatList.remove_decreases_count [in Lists]
NatList.rev_involutive [in Lists]
NatList.rev_length [in Lists]
NatList.rev_length_firsttry [in Lists]
NatList.snd_fst_is_swap [in Lists]
NatList.snoc_append [in Lists]
NatList.surjective_pairing [in Lists]
NatList.surjective_pairing' [in Lists]
NatList.surjective_pairing_stuck [in Lists]
NatList.tl_length_pred [in Lists]
negation_study_1 [in UseAuto]
negation_study_2 [in UseAuto]
negb_involutive [in Basics]
next_nat_closure_is_le [in Rel]
next_nat_partial_function [in Rel]
nf_is_value [in Smallstep]
nf_same_as_value [in Smallstep]
nil_app [in Poly]
nonsense_implies_False [in Logic]
normalization [in Norm]
normal_forms_unique [in Smallstep]
not_both_true_and_false [in Logic]
not_eq_beq_false [in Logic]
not_eq_beq_false [in SfLib]
not_eq_beq_id_false [in SfLib]
not_eq_beq_id_false [in ImpList]
not_ev_ev_S [in Hoare]
not_ev_ev_S_gen [in Hoare]
not_exists_dist [in Logic]
not_False [in Logic]
not_false_then_true [in Logic]
no_whiles_eqv [in Imp]
n_le_m__Sn_le_Sm [in Logic]
O
okdw' [in Prop]okd_before2_valid [in Prop]
omega_demo_1 [in UseAuto]
omega_demo_2 [in UseAuto]
omega_demo_3 [in UseAuto]
omega_demo_4 [in UseAuto]
orb_false [in Logic]
orb_true [in Logic]
order_matters_1 [in UseAuto]
order_matters_2 [in UseAuto]
or_commut [in Logic]
or_commut' [in Logic]
or_distributes_over_and [in Logic]
or_distributes_over_and_1 [in Logic]
or_distributes_over_and_2 [in Logic]
override_eq [in Poly]
override_example [in Poly]
override_neq [in Poly]
override_permute [in Poly]
override_same [in Poly]
override_shadow [in Poly]
O_le_n [in Logic]
P
pe_add_correct [in PE]pe_aexp_correct [in PE]
pe_aexp_correct_weak [in PE]
pe_bexp_correct [in PE]
pe_block_correct [in PE]
pe_compare_correct [in PE]
pe_compare_override [in PE]
pe_compare_removes [in PE]
pe_com_complete [in PE]
pe_com_correct [in PE]
pe_com_sound [in PE]
pe_consistent_override [in PE]
pe_disagree_domain [in PE]
pe_domain [in PE]
pe_override_consistent [in PE]
pe_override_correct [in PE]
pe_override_update_add [in PE]
pe_override_update_remove [in PE]
pe_program_correct [in PE]
pe_removes_correct [in PE]
pe_remove_correct [in PE]
pe_unique_correct [in PE]
pigeonhole_principle [in Logic]
plus2_spec [in Imp]
plus_assoc [in Basics]
plus_assoc' [in Basics]
plus_assoc' [in Prop]
plus_ble_compat_l [in Basics]
plus_comm [in Basics]
plus_comm' [in Prop]
plus_comm'' [in Prop]
plus_fact_is_true [in Prop]
plus_id_example [in Basics]
plus_id_exercise [in Basics]
plus_lt [in Logic]
plus_n_n_injective [in Poly]
plus_n_n_injective_take2 [in Gen]
plus_n_Sm [in Basics]
plus_one_r' [in Prop]
plus_O_n [in Basics]
plus_O_n' [in Basics]
plus_O_n'' [in Basics]
plus_rearrange [in Basics]
plus_rearrange_firsttry [in Basics]
plus_swap [in Basics]
plus_swap' [in Basics]
plus_0_r [in Basics]
plus_0_r_firsttry [in Basics]
plus_0_r_secondtry [in Basics]
plus_1_l [in Basics]
plus_1_neq_0 [in Basics]
plus_1_neq_0_firsttry [in Basics]
plus_2_2_is_4 [in Prop]
preservation [in Types]
preservation [in Subtyping]
preservation [in Norm]
preservation [in RecordSub]
PreservationProgressReferences.nth_eq_snoc' [in UseAuto]
PreservationProgressReferences.preservation [in UseAuto]
PreservationProgressReferences.preservation' [in UseAuto]
PreservationProgressReferences.preservation_ref [in UseAuto]
PreservationProgressReferences.progress [in UseAuto]
PreservationProgressStlc.preservation [in UseAuto]
PreservationProgressStlc.preservation' [in UseAuto]
PreservationProgressStlc.progress [in UseAuto]
PreservationProgressStlc.progress' [in UseAuto]
preservation' [in Types]
progress [in Subtyping]
progress [in Types]
progress [in RecordSub]
proj1 [in Logic]
proj2 [in Logic]
R
random_fact_1 [in Hoare]random_fact_2 [in Hoare]
rcd_types_match [in RecordSub]
reduce_to_zero_correct [in Hoare]
refl_aequiv [in Equiv]
refl_bequiv [in Equiv]
refl_cequiv [in Equiv]
rev_equation [in Hoare]
rev_exercise1 [in Poly]
rev_snoc [in Poly]
RingDemo.ring_demo [in UseAuto]
rsc_R [in SfLib]
rsc_R [in Rel]
rsc_trans [in SfLib]
rsc_trans [in Rel]
rtc_rsc_coincide [in Rel]
R_halts [in Norm]
R_typable_empty [in Norm]
S
search_depth_0 [in UseAuto]search_depth_1 [in UseAuto]
search_depth_3 [in UseAuto]
search_depth_4 [in UseAuto]
search_depth_5 [in UseAuto]
Semantics.stepmany__eval [in UseAuto]
Semantics.stepmany__eval' [in UseAuto]
seq_assoc [in Equiv]
sillyfun1_odd [in Poly]
sillyfun1_odd_FAILED [in Poly]
sillyfun_false [in Poly]
silly1 [in Poly]
silly2 [in Poly]
silly2a [in Poly]
silly3 [in Poly]
silly3' [in Poly]
silly3_firsttry [in Poly]
silly4 [in Poly]
silly5 [in Poly]
silly6 [in Poly]
silly7 [in Poly]
silly_ex [in Poly]
SimpleArith2.step_deterministic [in Smallstep]
SkipExample.ceval_deterministic [in UseTactics]
SkipExample.demo_skipH [in UseTactics]
SkipExample.mult_0_plus [in UseTactics]
skip_left [in Equiv]
skip_right [in Equiv]
snoc_equation [in Hoare]
snoc_with_append [in Poly]
Sn_le_Sm__n_le_m [in Logic]
solved_by_jauto [in UseAuto]
solving_by_apply [in UseAuto]
solving_by_apply' [in UseAuto]
solving_by_eapply [in UseAuto]
solving_by_reflexivity [in UseAuto]
solving_conj_goal [in UseAuto]
solving_conj_hyp [in UseAuto]
solving_conj_hyp' [in UseAuto]
solving_conj_hyp_forall [in UseAuto]
solving_conj_more [in UseAuto]
solving_disj_goal [in UseAuto]
solving_disj_hyp [in UseAuto]
solving_exists_goal [in UseAuto]
solving_exists_hyp [in UseAuto]
solving_tauto [in UseAuto]
SortExamples.ceval_deterministic [in UseTactics]
soundness [in Types]
sqrt_com_correct [in Hoare]
SSev_even [in Prop]
SSev_ev_firsttry [in Prop]
SSSSev_even [in Prop]
stepmany_App2 [in Norm]
stepmany_congr_1 [in Smallstep]
stepmany_congr_2 [in Smallstep]
stepmany_iff_eval [in Smallstep]
stepmany_preserves_R [in Norm]
stepmany_preserves_R' [in Norm]
stepmany__eval [in Smallstep]
step_deterministic [in Norm]
step_deterministic [in Smallstep]
step_deterministic [in Types]
step_normalizing [in Smallstep]
step_preserves_halting [in Norm]
step_preserves_R [in Norm]
step_preserves_record_tm [in RecordSub]
step_preserves_R' [in Norm]
step__eval [in Smallstep]
stequiv_aeval [in Equiv]
stequiv_beval [in Equiv]
stequiv_ceval [in Equiv]
stequiv_refl [in Equiv]
stequiv_sym [in Equiv]
stequiv_trans [in Equiv]
stequiv_update [in Equiv]
STLCChecker.beq_ty_refl [in Typechecking]
STLCChecker.beq_ty__eq [in Typechecking]
STLCChecker.type_checking_complete [in Typechecking]
STLCChecker.type_checking_sound [in Typechecking]
STLCExtendedRecords.context_invariance [in Records]
STLCExtendedRecords.free_in_context [in Records]
STLCExtendedRecords.has_type__wf [in Records]
STLCExtendedRecords.lookup_field_in_value [in Records]
STLCExtendedRecords.preservation [in Records]
STLCExtendedRecords.progress [in Records]
STLCExtendedRecords.step_preserves_record_tm [in Records]
STLCExtendedRecords.substitution_preserves_typing [in Records]
STLCExtendedRecords.typing_example_2 [in Records]
STLCExtendedRecords.wf_rcd_lookup [in Records]
STLCExtended.context_invariance [in MoreStlc]
STLCExtended.free_in_context [in MoreStlc]
STLCExtended.preservation [in MoreStlc]
STLCExtended.progress [in MoreStlc]
STLCExtended.substitution_preserves_typing [in MoreStlc]
STLCRef.assign_pres_store_typing [in References]
STLCRef.context_invariance [in References]
STLCRef.extends_lookup [in References]
STLCRef.extends_refl [in References]
STLCRef.extends_snoc [in References]
STLCRef.factorial_type [in References]
STLCRef.free_in_context [in References]
STLCRef.length_extends [in References]
STLCRef.length_replace [in References]
STLCRef.length_snoc [in References]
STLCRef.lookup_replace_eq [in References]
STLCRef.lookup_replace_neq [in References]
STLCRef.loop_fun_step_self [in References]
STLCRef.loop_steps_to_loop_fun [in References]
STLCRef.loop_typeable [in References]
STLCRef.nth_eq_snoc [in References]
STLCRef.nth_lt_snoc [in References]
STLCRef.preservation [in References]
STLCRef.preservation_wrong1 [in References]
STLCRef.preservation_wrong2 [in References]
STLCRef.progress [in References]
STLCRef.replace_nil [in References]
STLCRef.store_weakening [in References]
STLCRef.store_well_typed_snoc [in References]
STLCRef.substitution_preserves_typing [in References]
STLC.Context.extend_eq [in Stlc]
STLC.Context.extend_neq [in Stlc]
STLC.context_invariance [in Stlc]
STLC.free_in_context [in Stlc]
STLC.preservation [in Stlc]
STLC.progress [in Stlc]
STLC.progress' [in Stlc]
STLC.step_example1 [in Stlc]
STLC.step_example1' [in Stlc]
STLC.step_example2 [in Stlc]
STLC.step_example2' [in Stlc]
STLC.step_example3 [in Stlc]
STLC.substitution_preserves_typing [in Stlc]
STLC.typable_empty__closed [in Stlc]
strong_progress [in Smallstep]
substitution_preserves_typing [in Subtyping]
substitution_preserves_typing [in Norm]
substitution_preserves_typing [in RecordSub]
subst_closed [in Norm]
subst_inequiv [in Equiv]
subst_msubst [in Norm]
subst_not_afi [in Norm]
subtract_slowly_correct [in Hoare]
subtract_slowly_dec_correct [in Hoare]
subtype__wf [in RecordSub]
SubtypingInversion.abs_arrow [in UseAuto]
SubtypingInversion.abs_arrow' [in UseAuto]
SubtypingInversion.substitution_preserves_typing [in UseAuto]
sub_inversion_arrow [in RecordSub]
sub_inversion_arrow [in Subtyping]
sub_inversion_Bool [in Subtyping]
swap_if_branches [in Equiv]
swap_noninterfering_assignments [in Equiv]
swap_subst [in Norm]
sym_aequiv [in Equiv]
sym_bequiv [in Equiv]
sym_cequiv [in Equiv]
s_compile_correct [in Imp]
S_inj [in Poly]
S_nbeq_0 [in Basics]
T
Temp1.value_not_same_as_normal_form [in Smallstep]Temp2.value_not_same_as_normal_form [in Smallstep]
Temp3.value_not_same_as_normal_form [in Smallstep]
Temp4.step_deterministic [in Smallstep]
Temp4.strong_progress [in Smallstep]
test_le1 [in Logic]
test_le2 [in Logic]
test_le3 [in Logic]
test_stepmany_1 [in Smallstep]
test_stepmany_1' [in Smallstep]
test_stepmany_2 [in Smallstep]
test_stepmany_3 [in Smallstep]
test_stepmany_4 [in Smallstep]
transitivity_bad_hint_1 [in UseAuto]
transitivity_workaround_1 [in UseAuto]
transitivity_workaround_2 [in UseAuto]
trans_aequiv [in Equiv]
trans_bequiv [in Equiv]
trans_cequiv [in Equiv]
trans_eq [in Poly]
typable_empty__closed [in Norm]
typing_inversion_abs [in RecordSub]
typing_inversion_abs [in Subtyping]
typing_inversion_app [in RecordSub]
typing_inversion_app [in Subtyping]
typing_inversion_false [in Subtyping]
typing_inversion_if [in Subtyping]
typing_inversion_proj [in RecordSub]
typing_inversion_rcons [in RecordSub]
typing_inversion_true [in Subtyping]
typing_inversion_unit [in Subtyping]
typing_inversion_var [in RecordSub]
typing_inversion_var [in Subtyping]
U
uncurry_curry [in Poly]UnfoldsExample.bexp_eval_true [in UseTactics]
unfold_example [in Poly]
unfold_example_bad [in Poly]
update_eq [in ImpList]
update_eq [in Imp]
update_example [in Imp]
update_neq [in ImpList]
update_neq [in Imp]
update_permute [in Imp]
update_permute [in ImpList]
update_same [in Imp]
update_same [in ImpList]
update_shadow [in Imp]
update_shadow [in ImpList]
V
vacuous_substitution [in Norm]value_halts [in Norm]
value_is_nf [in Smallstep]
value_is_nf [in Types]
value__normal [in Norm]
verification_correct [in Hoare]
W
wf_rcd_lookup [in RecordSub]WHILE_false [in Equiv]
WHILE_true [in Equiv]
WHILE_true_nonterm [in Equiv]
working_of_auto_1 [in UseAuto]
working_of_auto_2 [in UseAuto]
Z
zero_nbeq_plus_1 [in Basics]zero_nbeq_S [in Basics]
Section Index
D
DemoAbsurd1 [in UseAuto]E
equatesLemma [in LibTactics]H
HintsTransitivity [in UseAuto]S
STLCRef.RefsAndNontermination [in References]Notation Index
A
AExp.aevalR_first_try.:type_scope:x_'||'_x [in Imp]AExp.:type_scope:x_'||'_x [in Imp]
C
CImp.::x_'/'_x_'==>'_x_'/'_x [in Smallstep]CImp.::x_'/'_x_'==>*'_x_'/'_x [in Smallstep]
CImp.::x_'::='_x [in Smallstep]
CImp.::x_';'_x [in Smallstep]
CImp.::'IFB'_x_'THEN'_x_'ELSE'_x_'FI' [in Smallstep]
CImp.::'PAR'_x_'WITH'_x_'END' [in Smallstep]
CImp.::'SKIP' [in Smallstep]
CImp.::'WHILE'_x_'DO'_x_'END' [in Smallstep]
Combined.::x_'==>'_x [in Smallstep]
L
Loop.::x_'/'_x_'/'_x_'/'_x_'||'_x_'#'_x [in PE]Loop.::x_'/'_x_'||'_x_'#'_x [in PE]
Loop.::x_'/'_x_'||'_x_'/'_x_'/'_x [in PE]
M
MyEquality.:type_scope:x_'='''_x [in Logic]MyEquality.:type_scope:x_'='_x [in Logic]
N
NatList.::x_'++'_x [in Lists]NatList.::x_'::'_x [in Lists]
NatList.::'('_x_','_x_')' [in Lists]
NatList.::'['_x_','_'..'_','_x_']' [in Lists]
NatList.::'['_']' [in Lists]
R
RepeatExercise.::x_'/'_x_'||'_x [in Hoare]RepeatExercise.::x_'::='_x [in Hoare]
RepeatExercise.::x_';'_x [in Hoare]
RepeatExercise.::'IFB'_x_'THEN'_x_'ELSE'_x_'FI' [in Hoare]
RepeatExercise.::'REPEAT'_x_'UNTIL'_x_'END' [in Hoare]
RepeatExercise.::'SKIP' [in Hoare]
RepeatExercise.::'WHILE'_x_'DO'_x_'END' [in Hoare]
RepeatExercise.::'{{'_x_'}}'_x_'{{'_x_'}}' [in Hoare]
S
SimpleArith1.::x_'||'_x [in Smallstep]SimpleArith2.::x_'==>'_x [in Smallstep]
STLCExtendedRecords.::x_'==>'_x [in Records]
STLCExtendedRecords.::x_'==>*'_x [in Records]
STLCExtended.::x_'==>'_x [in MoreStlc]
STLCExtended.::x_'==>*'_x [in MoreStlc]
STLCRef.RefsAndNontermination.::x_'/'_x_'==>+'_x_'/'_x [in References]
STLCRef.::x_'/'_x_'==>'_x_'/'_x [in References]
STLCRef.::x_'/'_x_'==>*'_x_'/'_x [in References]
STLC.::x_'==>'_x [in Stlc]
STLC.::x_'==>*'_x [in Stlc]
T
Temp1.::x_'==>'_x [in Smallstep]Temp2.::x_'==>'_x [in Smallstep]
Temp3.::x_'==>'_x [in Smallstep]
Temp4.Temp5.::x_'==>'_x [in Smallstep]
Temp4.::x_'==>'_x [in Smallstep]
:
:dcom_scope:x_'::='_x_'{{'_x_'}}' [in Hoare]:dcom_scope:x_';'_x [in Hoare]
:dcom_scope:x_'=>'_'{{'_x_'}}' [in Hoare]
:dcom_scope:'IFB'_x_'THEN'_'{{'_x_'}}'_x_'ELSE'_'{{'_x_'}}'_x_'FI' [in Hoare]
:dcom_scope:'SKIP'_'{{'_x_'}}' [in Hoare]
:dcom_scope:'WHILE'_x_'DO'_'{{'_x_'}}'_x_'END'_'{{'_x_'}}' [in Hoare]
:dcom_scope:'=>'_'{{'_x_'}}'_x [in Hoare]
:dcom_scope:'{{'_x_'}}'_x [in Hoare]
:hoare_spec_scope:'{{'_x_'}}'_x [in Hoare]
:hoare_spec_scope:'{{'_x_'}}'_x_'{{'_x_'}}' [in Hoare]
:ltac_scope:'>>' [in LibTactics]
:ltac_scope:'>>'_x [in LibTactics]
:ltac_scope:'>>'_x_x [in LibTactics]
:ltac_scope:'>>'_x_x_x [in LibTactics]
:ltac_scope:'>>'_x_x_x_x [in LibTactics]
:ltac_scope:'>>'_x_x_x_x_x [in LibTactics]
:ltac_scope:'>>'_x_x_x_x_x_x [in LibTactics]
:ltac_scope:'>>'_x_x_x_x_x_x_x [in LibTactics]
:ltac_scope:'>>'_x_x_x_x_x_x_x_x [in LibTactics]
:ltac_scope:'>>'_x_x_x_x_x_x_x_x_x [in LibTactics]
:ltac_scope:'>>'_x_x_x_x_x_x_x_x_x_x [in LibTactics]
:ltac_scope:'>>'_x_x_x_x_x_x_x_x_x_x_x [in LibTactics]
:ltac_scope:'>>'_x_x_x_x_x_x_x_x_x_x_x_x [in LibTactics]
:ltac_scope:'>>'_x_x_x_x_x_x_x_x_x_x_x_x_x [in LibTactics]
:ltac_scope:'__' [in LibTactics]
:ltac_scope:'___' [in LibTactics]
:nat_scope:x_'*'_x [in Basics]
:nat_scope:x_'+'_x [in Basics]
:nat_scope:x_'-'_x [in Basics]
:nat_scope:x_'<=?'_x [in ImpParser]
:type_scope:x_'*'_x [in Poly]
:type_scope:x_'/\'_x [in Logic]
:type_scope:x_'<->'_x [in Logic]
:type_scope:x_'<>'_x [in Logic]
:type_scope:x_'\/'_x [in Logic]
:type_scope:'exists'_x_x_x_x_x_x_x_x_x_x_','_x [in LibTactics]
:type_scope:'exists'_x_x_x_x_x_x_x_x_x_','_x [in LibTactics]
:type_scope:'exists'_x_x_x_x_x_x_x_x_','_x [in LibTactics]
:type_scope:'exists'_x_x_x_x_x_x_x_','_x [in LibTactics]
:type_scope:'exists'_x_x_x_x_x_x_','_x [in LibTactics]
:type_scope:'exists'_x_x_x_x_x_','_x [in LibTactics]
:type_scope:'exists'_x_x_x_x_','_x [in LibTactics]
:type_scope:'exists'_x_x_x_','_x [in LibTactics]
:type_scope:'exists'_x_x_','_x [in LibTactics]
:type_scope:'exists'_x_','_x [in Logic]
:type_scope:'exists'_x_','_x [in LibTactics]
:type_scope:'exists'_x_':'_x_','_x [in Logic]
:type_scope:'~'_x [in Logic]
::x_'++'_x [in SfLib]
::x_'++'_x [in Poly]
::x_'/'_x_'/'_x_'||'_x [in PE]
::x_'/'_x_'==>a'_x [in Smallstep]
::x_'/'_x_'==>a*'_x [in Types]
::x_'/'_x_'==>b'_x [in Smallstep]
::x_'/'_x_'==>'_x_'/'_x [in Smallstep]
::x_'/'_x_'||'''_x [in Equiv]
::x_'/'_x_'||'_x [in Imp]
::x_'/'_x_'||'_x [in ImpList]
::x_'/'_x_'||'_x_'/'_x [in PE]
::x_'::'_x [in Poly]
::x_'::='_x [in Imp]
::x_'::='_x [in ImpList]
::x_';'_x [in Imp]
::x_';'_x [in ImpList]
::x_'<'_x [in Logic]
::x_'<='_x [in Logic]
::x_'<~~>'_x [in Hoare]
::x_'='''_x [in LibTactics]
::x_'==>'_x [in Types]
::x_'==>'_x [in Norm]
::x_'==>'_x [in Subtyping]
::x_'==>'_x [in RecordSub]
::x_'==>'_x [in Smallstep]
::x_'==>*'_x [in Smallstep]
::x_'==>*'_x [in Types]
::x_'==>*'_x [in Norm]
::x_'||'_x [in Smallstep]
::x_'~'_x [in Equiv]
::x_'~~>'_x [in Hoare]
::'DO'_'('_x_','_x_')'_'<--'_x_';;'_x_'OR'_x [in ImpParser]
::'DO'_'('_x_','_x_')'_'<=='_x_';;'_x [in ImpParser]
::'IFB'_x_'THEN'_x_'ELSE'_x_'FI' [in Imp]
::'IFB'_x_'THEN'_x_'ELSE'_x_'FI' [in ImpList]
::'LETOPT'_x_'<=='_x_'IN'_x [in Imp]
::'nosimpl'_x [in LibTactics]
::'Register'_x_x [in LibTactics]
::'SKIP' [in ImpList]
::'SKIP' [in Imp]
::'Something' [in LibTactics]
::'WHILE'_x_'DO'_x_'END' [in Imp]
::'WHILE'_x_'DO'_x_'END' [in ImpList]
::'('_x_','_x_')' [in Poly]
::'['_x_','_'..'_','_x_']' [in Poly]
::'['_x_','_'..'_','_x_']' [in SfLib]
::'['_']' [in Poly]
::'['_']' [in SfLib]
Constructor Index
A
ACons [in ImpList]AExp.aevalR_first_try.E_AMinus [in Imp]
AExp.aevalR_first_try.E_AMult [in Imp]
AExp.aevalR_first_try.E_ANum [in Imp]
AExp.aevalR_first_try.E_APlus [in Imp]
AExp.AMinus [in Imp]
AExp.AMult [in Imp]
AExp.ANum [in Imp]
AExp.APlus [in Imp]
AExp.BAnd [in Imp]
AExp.BEq [in Imp]
AExp.BFalse [in Imp]
AExp.BLe [in Imp]
AExp.BNot [in Imp]
AExp.BTrue [in Imp]
AExp.E_AMinus [in Imp]
AExp.E_AMult [in Imp]
AExp.E_ANum [in Imp]
AExp.E_APlus [in Imp]
afi_abs [in RecordSub]
afi_abs [in Norm]
afi_abs [in Subtyping]
afi_app1 [in RecordSub]
afi_app1 [in Subtyping]
afi_app1 [in Norm]
afi_app2 [in Subtyping]
afi_app2 [in Norm]
afi_app2 [in RecordSub]
afi_fst [in Norm]
afi_if0 [in Norm]
afi_if1 [in Subtyping]
afi_if1 [in Norm]
afi_if2 [in Norm]
afi_if2 [in Subtyping]
afi_if3 [in Subtyping]
afi_pair1 [in Norm]
afi_pair2 [in Norm]
afi_proj [in RecordSub]
afi_rhead [in RecordSub]
afi_rtail [in RecordSub]
afi_snd [in Norm]
afi_var [in RecordSub]
afi_var [in Subtyping]
afi_var [in Norm]
AHead [in ImpList]
AId [in ImpList]
AId [in Imp]
ai_here [in Logic]
ai_here [in SfLib]
ai_later [in SfLib]
ai_later [in Logic]
alpha [in ImpParser]
AMinus [in Imp]
AMinus [in ImpList]
AMult [in ImpList]
AMult [in Imp]
ANil [in ImpList]
ANum [in Imp]
ANum [in ImpList]
APlus [in ImpList]
APlus [in Imp]
Assign [in PE]
AS_Id [in Smallstep]
AS_Minus [in Smallstep]
AS_Minus1 [in Smallstep]
AS_Minus2 [in Smallstep]
AS_Mult [in Smallstep]
AS_Mult1 [in Smallstep]
AS_Mult2 [in Smallstep]
AS_Plus [in Smallstep]
AS_Plus1 [in Smallstep]
AS_Plus2 [in Smallstep]
ATail [in ImpList]
av_num [in Smallstep]
B
BAnd [in ImpList]BAnd [in Imp]
BEq [in ImpList]
BEq [in Imp]
BFalse [in ImpList]
BFalse [in Imp]
BIsCons [in ImpList]
BLe [in Imp]
BLe [in ImpList]
blue [in Prop]
BNot [in ImpList]
BNot [in Imp]
body [in PE]
bool_cons [in Poly]
bool_nil [in Poly]
boxer [in LibTactics]
BS_AndFalse [in Smallstep]
BS_AndStep [in Smallstep]
BS_AndTrueFalse [in Smallstep]
BS_AndTrueStep [in Smallstep]
BS_AndTrueTrue [in Smallstep]
BS_Eq [in Smallstep]
BS_Eq1 [in Smallstep]
BS_Eq2 [in Smallstep]
BS_LtEq [in Smallstep]
BS_LtEq1 [in Smallstep]
BS_LtEq2 [in Smallstep]
BS_NotFalse [in Smallstep]
BS_NotStep [in Smallstep]
BS_NotTrue [in Smallstep]
BTrue [in ImpList]
BTrue [in Imp]
bv_false [in Types]
bv_true [in Types]
C
CAss [in Imp]CAss [in ImpList]
CIf [in Imp]
CIf [in ImpList]
CImp.CAss [in Smallstep]
CImp.CIf [in Smallstep]
CImp.CPar [in Smallstep]
CImp.CSeq [in Smallstep]
CImp.CSkip [in Smallstep]
CImp.CS_Ass [in Smallstep]
CImp.CS_AssStep [in Smallstep]
CImp.CS_IfFalse [in Smallstep]
CImp.CS_IfStep [in Smallstep]
CImp.CS_IfTrue [in Smallstep]
CImp.CS_ParDone [in Smallstep]
CImp.CS_Par1 [in Smallstep]
CImp.CS_Par2 [in Smallstep]
CImp.CS_SeqFinish [in Smallstep]
CImp.CS_SeqStep [in Smallstep]
CImp.CS_While [in Smallstep]
CImp.CWhile [in Smallstep]
Combined.ST_If [in Smallstep]
Combined.ST_IfFalse [in Smallstep]
Combined.ST_IfTrue [in Smallstep]
Combined.ST_PlusConstConst [in Smallstep]
Combined.ST_Plus1 [in Smallstep]
Combined.ST_Plus2 [in Smallstep]
Combined.tm_const [in Smallstep]
Combined.tm_false [in Smallstep]
Combined.tm_if [in Smallstep]
Combined.tm_plus [in Smallstep]
Combined.tm_true [in Smallstep]
Combined.v_const [in Smallstep]
Combined.v_false [in Smallstep]
Combined.v_true [in Smallstep]
conj [in Logic]
cons [in Poly]
CSeq [in Imp]
CSeq [in ImpList]
CSkip [in ImpList]
CSkip [in Imp]
CS_Ass [in Smallstep]
CS_AssStep [in Smallstep]
CS_IfFalse [in Smallstep]
CS_IfStep [in Smallstep]
CS_IfTrue [in Smallstep]
CS_SeqFinish [in Smallstep]
CS_SeqStep [in Smallstep]
CS_While [in Smallstep]
CWhile [in Imp]
CWhile [in ImpList]
C1 [in Prop]
C2 [in Prop]
D
db_fri [in Prop]db_mon [in Prop]
db_sat [in Prop]
db_sun [in Prop]
db_thu [in Prop]
db_tue [in Prop]
db_wed [in Prop]
DCAsgn [in Hoare]
DCIf [in Hoare]
DCPost [in Hoare]
DCPre [in Hoare]
DCSeq [in Hoare]
DCSkip [in Hoare]
DCWhile [in Hoare]
digit [in ImpParser]
done [in PE]
E