Global Index

(2463 entries)

Lemma Index

(710 entries)

Section Index

(4 entries)

Constructor Index

(768 entries)

Abbreviation Index

(66 entries)

Inductive Index

(186 entries)

Definition Index

(610 entries)

Module Index

(69 entries)

Axiom Index

(12 entries)

Variable Index

(8 entries)

Library Index

(30 entries)

Global Index

A

abs_arrow [lemma, in Subtyping]
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]
aevalR_first_try [module, in Imp]
aeval_weakening [lemma, in Equiv]
aexp [inductive, in ImpList]
aexp [inductive, in Imp]
AExp [module, in Imp]
AExp.aeval [definition, in Imp]
AExp.aevalR [inductive, 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.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]
aexp1 [definition, in Imp]
afi_abs [constructor, in RecordSub]
afi_abs [constructor, in Norm]
afi_abs [constructor, in Subtyping]
afi_abs [constructor, in Subtyping]
afi_app1 [constructor, in RecordSub]
afi_app1 [constructor, in Subtyping]
afi_app1 [constructor, in Subtyping]
afi_app1 [constructor, in Norm]
afi_app2 [constructor, in Subtyping]
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 Subtyping]
afi_if1 [constructor, in Norm]
afi_if2 [constructor, in Norm]
afi_if2 [constructor, in Subtyping]
afi_if2 [constructor, in Subtyping]
afi_if3 [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 Subtyping]
afi_var [constructor, in Norm]
AHead [constructor, in ImpList]
AId [constructor, in Imp]
AId [constructor, in ImpList]
ai_here [constructor, in Logic]
ai_here [constructor, in SfLib]
ai_later [constructor, in Logic]
ai_later [constructor, in SfLib]
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 ImpList]
ANum [constructor, in Imp]
APlus [constructor, in Imp]
APlus [constructor, in ImpList]
app [definition, in Poly]
appears_free_in [inductive, in RecordSub]
appears_free_in [inductive, in Norm]
appears_free_in [inductive, in Subtyping]
appears_free_in [inductive, in Subtyping]
appears_in [inductive, in SfLib]
appears_in [inductive, in Logic]
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_length [lemma, in Logic]
app_length_cons [lemma, in Ind]
app_length_twice [lemma, in Ind]
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 Stlc]
astep_example1' [definition, in Stlc]
astep_example1'' [definition, in Stlc]
astep_example1''' [definition, in Stlc]
astep_many [definition, in Stlc]
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 Stlc]
auto_example_2 [lemma, in Stlc]
auto_example_2a [lemma, in Stlc]
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 SfLib]
beq_nat_sym [definition, in Lists]
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 Ind]
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 Imp]
BFalse [constructor, in ImpList]
BIsCons [constructor, in ImpList]
BLe [constructor, in ImpList]
BLe [constructor, in Imp]
ble_nat [definition, in Basics]
ble_nat [definition, in SfLib]
ble_nat_false [lemma, in SfLib]
ble_nat_false [lemma, in Logic]
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 Ind]
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 Stlc]
bv_false [constructor, in Stlc]
bv_true [constructor, in Stlc]

C

D

day [inductive, in Basics]
day_before [inductive, in Ind]
db_fri [constructor, in Ind]
db_mon [constructor, in Ind]
db_sat [constructor, in Ind]
db_sun [constructor, in Ind]
db_thu [constructor, in Ind]
db_tue [constructor, in Ind]
db_wed [constructor, in Ind]
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 UseTactics]
demo_false [lemma, in UseAuto]
demo_hint_unfold_context_1 [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]
Dictionary [module, in Lists]
Dictionary.dictionary [inductive, in Lists]
Dictionary.dictionary_invariant1 [lemma, in Lists]
Dictionary.dictionary_invariant2 [lemma, in Lists]
Dictionary.empty [constructor, in Lists]
Dictionary.find [definition, in Lists]
Dictionary.insert [definition, in Lists]
Dictionary.record [constructor, in Lists]
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 Ind]
double_injective [lemma, in Poly]
double_injective' [lemma, in Ind]
double_injective_FAILED [lemma, in Ind]
double_injective_take2 [lemma, in Ind]
double_injective_take2_FAILED [lemma, in Ind]
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

F

G

gds [lemma, in Ind]
gd_sat [constructor, in Ind]
gd_sun [constructor, in Ind]
GenExample [module, in UseTactics]
GenExample.substitution_preserves_typing [lemma, in UseTactics]
good_day [inductive, in Ind]
Goto [constructor, in PE]
green [constructor, in Ind]
gt_not_le [axiom, in UseAuto]
guard_false_after_loop [lemma, in Imp]

H

I

Id [module, in Imp]
id [inductive, in ImpList]
Id [constructor, in SfLib]
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 [inductive, in Imp]
Id.Id [constructor, 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]
Ind [library]
index [definition, in Poly]
index_after_last [lemma, in Ind]
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 Ind]
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 Ind]
LetTest [module, in MoreStlc]
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]
ListTest [module, in MoreStlc]
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_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 Ind]
mult_0_r'' [lemma, in Ind]
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]
myFact [definition, in UseAuto]
mynil [definition, in Poly]
mynil' [definition, in Poly]
MyProp [inductive, in Ind]
MyProp1 [constructor, in Ind]
MyProp2 [constructor, in Ind]
MyProp3 [constructor, in Ind]
MyProp_ev [lemma, in Ind]
MyProp_iff_ev [definition, in Logic]
MyProp_plustwo [lemma, in Ind]
MyProp_ten [lemma, in Ind]
MyProp_0 [lemma, in Ind]

N

O

oddb [definition, in Basics]
okdw [definition, in Ind]
okdw' [lemma, in Ind]
okd_before [constructor, in Ind]
okd_before2 [definition, in Ind]
okd_before2_valid [lemma, in Ind]
okd_before2_valid' [definition, in Ind]
okd_gd [constructor, in Ind]
ok_day [inductive, in Ind]
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 Ind]
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 [definition, in Logic]
P [module, in Ind]
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 Ind]
plus_assoc' [lemma, in Basics]
plus_ble_compat_l [lemma, in Basics]
plus_comm [lemma, in Basics]
plus_comm' [lemma, in Ind]
plus_comm'' [lemma, in Ind]
plus_fact [definition, in Ind]
plus_fact_is_true [lemma, in Ind]
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 Ind]
plus_n_Sm [lemma, in Basics]
plus_one_r' [lemma, in Ind]
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 Ind]
Poly [library]
post [definition, in Hoare]
Postscript [library]
pre [definition, in Hoare]
Preface [library]
preorder [definition, in Rel]
preservation [lemma, in Subtyping]
preservation [lemma, in Subtyping]
preservation [lemma, in Norm]
preservation [lemma, in RecordSub]
preservation [lemma, in Stlc]
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 Stlc]
preserved_by_S [definition, in Ind]
prod [inductive, in Poly]
Prodtest [module, in MoreStlc]
prod_curry [definition, in Poly]
prod_uncurry [definition, in Poly]
program [definition, in PE]
progress [lemma, in Subtyping]
progress [lemma, in Subtyping]
progress [lemma, in Stlc]
progress [lemma, in RecordSub]
proj1 [lemma, in Logic]
proj2 [lemma, in Logic]
pup_to_n [definition, in Imp]
P.c1 [constructor, in Ind]
P.c2 [constructor, in Ind]
P.c3 [constructor, in Ind]
P.p [inductive, in Ind]
P_m0r [definition, in Ind]
P_m0r' [definition, in Ind]

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 Ind]
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]
repeats [inductive, in Logic]
rev [definition, in Poly]
rev [definition, in Hoare]
rev_equation [lemma, in Hoare]
rev_snoc [lemma, in Poly]
rgb [inductive, in Ind]
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

T

tail [definition, in ImpList]
tass [definition, in Norm]
teen [definition, in Ind]
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]
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]
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]
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.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.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]
Temp5 [module, 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 Stlc]
tm [inductive, in Subtyping]
tm [inductive, in Subtyping]
tm_abs [constructor, in Norm]
tm_abs [constructor, in Subtyping]
tm_abs [constructor, in Subtyping]
tm_abs [constructor, in RecordSub]
tm_app [constructor, in Norm]
tm_app [constructor, in Subtyping]
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 Subtyping]
tm_false [constructor, in Stlc]
tm_fst [constructor, in Norm]
tm_if [constructor, in Norm]
tm_if [constructor, in Subtyping]
tm_if [constructor, in Subtyping]
tm_if [constructor, in Stlc]
tm_iszero [constructor, in Stlc]
tm_lookup [definition, in RecordSub]
tm_pair [constructor, in Norm]
tm_plus [constructor, in Smallstep]
tm_pred [constructor, in Stlc]
tm_proj [constructor, in RecordSub]
tm_rcons [constructor, in RecordSub]
tm_rnil [constructor, in RecordSub]
tm_snd [constructor, in Norm]
tm_succ [constructor, in Stlc]
tm_true [constructor, in Stlc]
tm_true [constructor, in Subtyping]
tm_true [constructor, in Subtyping]
tm_true [constructor, in Norm]
tm_unit [constructor, in Subtyping]
tm_unit [constructor, in Subtyping]
tm_var [constructor, in Norm]
tm_var [constructor, in Subtyping]
tm_var [constructor, in Subtyping]
tm_var [constructor, in RecordSub]
tm_zero [constructor, in Stlc]
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 Ind]
true [constructor, in Basics]
true_for_all_numbers [definition, in Ind]
true_for_n__true_for_Sn [definition, in Ind]
true_for_zero [definition, in Ind]
tuesday [constructor, in Basics]
ty [inductive, in Subtyping]
ty [inductive, in Subtyping]
ty [inductive, in RecordSub]
ty [inductive, in Norm]
ty [inductive, in Stlc]
typ [axiom, in UseAuto]
typable_empty__closed [lemma, in Norm]
Typechecking [library]
typing_inversion_abs [lemma, in RecordSub]
typing_inversion_abs [lemma, in Subtyping]
typing_inversion_abs [lemma, in Subtyping]
typing_inversion_app [lemma, in RecordSub]
typing_inversion_app [lemma, in Subtyping]
typing_inversion_app [lemma, in Subtyping]
typing_inversion_false [lemma, in Subtyping]
typing_inversion_false [lemma, in Subtyping]
typing_inversion_if [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_true [lemma, in Subtyping]
typing_inversion_unit [lemma, in Subtyping]
typing_inversion_unit [lemma, in Subtyping]
typing_inversion_var [lemma, in RecordSub]
typing_inversion_var [lemma, in Subtyping]
typing_inversion_var [lemma, in Subtyping]
ty_arrow [constructor, in RecordSub]
ty_arrow [constructor, in Subtyping]
ty_arrow [constructor, in Subtyping]
ty_arrow [constructor, in Norm]
ty_base [constructor, in RecordSub]
ty_base [constructor, in Subtyping]
ty_base [constructor, in Subtyping]
ty_Bool [constructor, in Norm]
ty_Bool [constructor, in Subtyping]
ty_Bool [constructor, in Subtyping]
ty_Bool [constructor, in Stlc]
ty_lookup [definition, in RecordSub]
ty_Nat [constructor, in Stlc]
ty_prod [constructor, in Norm]
ty_rcons [constructor, in RecordSub]
ty_rnil [constructor, in RecordSub]
ty_Top [constructor, in Subtyping]
ty_Top [constructor, in Subtyping]
ty_Top [constructor, in RecordSub]
ty_Unit [constructor, in Subtyping]
ty_Unit [constructor, in Subtyping]
T_Abs [constructor, in Norm]
T_Abs [constructor, in Subtyping]
T_Abs [constructor, in Subtyping]
T_Abs [constructor, in RecordSub]
T_App [constructor, in Subtyping]
T_App [constructor, in Subtyping]
T_App [constructor, in RecordSub]
T_App [constructor, in Norm]
t_false [constructor, in Subtyping]
t_false [constructor, in Subtyping]
T_False [constructor, in Stlc]
T_False [constructor, in Norm]
T_False [constructor, in Subtyping]
T_False [constructor, in Subtyping]
T_Fst [constructor, in Norm]
T_If [constructor, in Stlc]
T_If [constructor, in Norm]
T_If [constructor, in Subtyping]
T_If [constructor, in Subtyping]
T_Iszero [constructor, in Stlc]
T_Pair [constructor, in Norm]
T_Pred [constructor, in Stlc]
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_Sub [constructor, in Subtyping]
T_Succ [constructor, in Stlc]
t_true [constructor, in Subtyping]
t_true [constructor, in Subtyping]
T_True [constructor, in Norm]
T_True [constructor, in Stlc]
T_True [constructor, in Subtyping]
T_True [constructor, in Subtyping]
T_Unit [constructor, in Subtyping]
T_Unit [constructor, in Subtyping]
T_Var [constructor, in Norm]
T_Var [constructor, in RecordSub]
T_Var [constructor, in Subtyping]
T_Var [constructor, in Subtyping]
T_Zero [constructor, in Stlc]

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 Imp]
update_eq [lemma, in ImpList]
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 ImpList]
update_same [lemma, in Imp]
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 [inductive, in Subtyping]
value [definition, in Stlc]
value_halts [lemma, in Norm]
value_is_nf [lemma, in Smallstep]
value_is_nf [lemma, in Stlc]
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_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]
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 Imp]
X [definition, in ImpList]
XtimesYinZ [definition, in Imp]

Y

Y [definition, in ImpList]
Y [definition, in Imp]
yes [constructor, in Ind]
yesno [inductive, in Ind]

Z

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

Lemma Index

A

abs_arrow [in Subtyping]
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_length [in Logic]
app_length_cons [in Ind]
app_length_twice [in Ind]
assign_aequiv [in Equiv]
assign_removes [in PE]
auto_example_1 [in Stlc]
auto_example_2 [in Stlc]
auto_example_2a [in Stlc]

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 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 SfLib]
ble_nat_false [in Logic]
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_arrow_types [in Subtyping]
canonical_forms_of_Bool [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]
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 UseTactics]
demo_false [in UseAuto]
demo_hint_unfold_context_1 [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]
Dictionary.dictionary_invariant1 [in Lists]
Dictionary.dictionary_invariant2 [in Lists]
dist_exists_or [in Logic]
dist_not_exists [in Logic]
double_even [in Ind]
double_injective [in Poly]
double_injective' [in Ind]
double_injective_FAILED [in Ind]
double_injective_take2 [in Ind]
double_injective_take2_FAILED [in Ind]
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 Ind]
even_ev [in Logic]
even_ev' [in Logic]
ev_even [in Ind]
ev_even' [in Ind]
ev_ev_even [in Ind]
ev_minus2 [in Ind]
ev_minus2' [in Ind]
ev_MyProp [in Ind]
ev_MyProp' [in Ind]
ev_not_ev_S [in SfLib]
ev_not_ev_S [in Logic]
ev_plus4' [in Ind]
ev_plus_plus [in Ind]
ev_sum [in Ind]
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 Ind]
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 Ind]
free_in_context [in Subtyping]
free_in_context [in Subtyping]
free_in_context [in Norm]
free_in_context [in RecordSub]

G

gds [in Ind]
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 Ind]
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 Ind]
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 Ind]
mult_0_r'' [in Ind]
mult_1_l [in Basics]
mult_1_plus [in Basics]
MyEquality.two_defs_of_eq_coincide [in Logic]
MyProp_ev [in Ind]
MyProp_plustwo [in Ind]
MyProp_ten [in Ind]
MyProp_0 [in Ind]

N

O

okdw' [in Ind]
okd_before2_valid [in Ind]
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

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

T

U

uncurry_curry [in Poly]
UnfoldsExample.bexp_eval_true [in UseTactics]
unfold_example [in Poly]
unfold_example_bad [in Poly]
update_eq [in Imp]
update_eq [in ImpList]
update_example [in Imp]
update_neq [in ImpList]
update_neq [in Imp]
update_permute [in Imp]
update_permute [in ImpList]
update_same [in ImpList]
update_same [in Imp]
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 Stlc]
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]

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_abs [in Subtyping]
afi_app1 [in RecordSub]
afi_app1 [in Subtyping]
afi_app1 [in Subtyping]
afi_app1 [in Norm]
afi_app2 [in Subtyping]
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 Subtyping]
afi_if1 [in Norm]
afi_if2 [in Norm]
afi_if2 [in Subtyping]
afi_if2 [in Subtyping]
afi_if3 [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 Subtyping]
afi_var [in Norm]
AHead [in ImpList]
AId [in Imp]
AId [in ImpList]
ai_here [in Logic]
ai_here [in SfLib]
ai_later [in Logic]
ai_later [in SfLib]
alpha [in ImpParser]
AMinus [in Imp]
AMinus [in ImpList]
AMult [in ImpList]
AMult [in Imp]
ANil [in ImpList]
ANum [in ImpList]
ANum [in Imp]
APlus [in Imp]
APlus [in ImpList]
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 Imp]
BFalse [in ImpList]
BIsCons [in ImpList]
BLe [in ImpList]
BLe [in Imp]
blue [in Ind]
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 Stlc]
bv_true [in Stlc]

C

D

db_fri [in Ind]
db_mon [in Ind]
db_sat [in Ind]
db_sun [in Ind]
db_thu [in Ind]
db_tue [in Ind]
db_wed [in Ind]
DCAsgn [in Hoare]
DCIf [in Hoare]
DCPost [in Hoare]
DCPre [in Hoare]
DCSeq [in Hoare]
DCSkip [in Hoare]
DCWhile [in Hoare]
Dictionary.empty [in Lists]
Dictionary.record [in Lists]
digit [in ImpParser]
done [in PE]

E

entry [in PE]
ev_SS [in Ind]
ev_SS [in SfLib]
ev_0 [in Ind]
ev_0 [in SfLib]
ex_intro [in Logic]
E_Asgn [in ImpList]
E_Ass [in Imp]
E_Const [in Smallstep]
E_equiv [in Equiv]
E_IfFalse [in ImpList]
E_IfFalse [in Imp]
E_IfTrue [in Imp]
E_IfTrue [in ImpList]
E_None [in PE]
E_Plus [in Smallstep]
E_Seq [in Imp]
E_Seq [in ImpList]
E_Skip [in Imp]
E_Skip [in ImpList]
E_Some [in PE]
E_WhileEnd [in ImpList]
E_WhileEnd [in Imp]
E_WhileLoop [in Imp]
E_WhileLoop [in ImpList]

F

false [in Basics]
fdfs_any [in Ind]
friday [in Basics]

G

gd_sat [in Ind]
gd_sun [in Ind]
Goto [in PE]
green [in Ind]

H

H_Asgn [in HoareAsLogic]
H_Consequence [in HoareAsLogic]
H_Consequence_post [in HoareAsLogic]
H_Consequence_pre [in HoareAsLogic]
H_If [in HoareAsLogic]
H_Seq [in HoareAsLogic]
H_Skip [in HoareAsLogic]
H_While [in HoareAsLogic]

I

Id [in SfLib]
Id [in ImpList]
Id.Id [in Imp]
If [in PE]

L

leaf [in Ind]
LeFirstTry.le_n [in Logic]
LeFirstTry.le_S [in Logic]
le_n [in Logic]
le_S [in Logic]
loop [in PE]
Loop.E'Ass [in PE]
Loop.E'IfFalse [in PE]
Loop.E'IfTrue [in PE]
Loop.E'Seq [in PE]
Loop.E'Skip [in PE]
Loop.E'WhileEnd [in PE]
Loop.E'WhileLoop [in PE]
Loop.PE_AssDynamic [in PE]
Loop.PE_AssStatic [in PE]
Loop.pe_ceval_count_intro [in PE]
Loop.PE_If [in PE]
Loop.PE_IfFalse [in PE]
Loop.PE_IfTrue [in PE]
Loop.PE_Seq [in PE]
Loop.PE_Skip [in PE]
Loop.PE_While [in PE]
Loop.PE_WhileEnd [in PE]
Loop.PE_WhileFixed [in PE]
Loop.PE_WhileFixedEnd [in PE]
Loop.PE_WhileFixedLoop [in PE]
Loop.PE_WhileLoop [in PE]
ltac_mark [in LibTactics]
ltac_no_arg [in LibTactics]
ltac_wild [in LibTactics]
ltac_wilds [in LibTactics]

M

monday [in Basics]
MumbleBaz.a [in Poly]
MumbleBaz.b [in Poly]
MumbleBaz.c [in Poly]
MumbleBaz.d [in Poly]
MumbleBaz.e [in Poly]
MumbleBaz.x [in Poly]
MumbleBaz.y [in Poly]
MyEquality.refl_equal [in Logic]
MyEquality.refl_equal' [in Logic]
MyProp1 [in Ind]
MyProp2 [in Ind]
MyProp3 [in Ind]

N

NatList.cons [in Lists]
NatList.nil [in Lists]
NatList.None [in Lists]
NatList.pair [in Lists]
NatList.Some [in Lists]
ncons [in Ind]
ne_1 [in Logic]
ne_2 [in Logic]
nil [in Poly]
nn [in Logic]
nn [in SfLib]
nnil [in Ind]
nnil1 [in Ind]
no [in Ind]
node [in Ind]
None [in Poly]
NoneE [in ImpParser]
nsnoc1 [in Ind]
nv_succ [in Stlc]
nv_zero [in Stlc]

O

okd_before [in Ind]
okd_gd [in Ind]
or_introl [in Logic]
or_intror [in Logic]
other [in ImpParser]

P

pair [in Poly]
PE_AssDynamic [in PE]
PE_AssStatic [in PE]
pe_ceval_intro [in PE]
PE_If [in PE]
PE_IfFalse [in PE]
PE_IfTrue [in PE]
pe_peval_intro [in PE]
PE_Seq [in PE]
PE_Skip [in PE]
Playground1.O [in Basics]
Playground1.S [in Basics]
P.c1 [in Ind]
P.c2 [in Ind]
P.c3 [in Ind]

R

S

T

V

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

W

wednesday [in Basics]
wfty_arrow [in RecordSub]
wfty_base [in RecordSub]
wfty_rcons [in RecordSub]
wfty_rnil [in RecordSub]
wfty_Top [in RecordSub]
white [in ImpParser]

Y

yes [in Ind]

Abbreviation Index

E

S

Inductive Index

A

aexp [in ImpList]
aexp [in Imp]
AExp.aevalR [in Imp]
AExp.aevalR_first_try.aevalR [in Imp]
AExp.aexp [in Imp]
AExp.bexp [in Imp]
all [in Logic]
and [in Logic]
appears_free_in [in RecordSub]
appears_free_in [in Norm]
appears_free_in [in Subtyping]
appears_free_in [in Subtyping]
appears_in [in SfLib]
appears_in [in Logic]
astep [in Smallstep]
aval [in Smallstep]

B

bexp [in ImpList]
bexp [in Imp]
block [in PE]
bool [in Basics]
boollist [in Poly]
Boxer [in LibTactics]
bstep [in Smallstep]
bvalue [in Stlc]

C

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

D

day [in Basics]
day_before [in Ind]
dcom [in Hoare]
Dictionary.dictionary [in Lists]

E

empty_relation [in SfLib]
ev [in SfLib]
ev [in Ind]
eval [in Smallstep]
ex [in Logic]
ExSet [in Ind]

F

False [in Logic]
fine_day_for_singing [in Ind]
foo' [in Ind]

G

good_day [in Ind]

H

has_type [in RecordSub]
has_type [in Subtyping]
has_type [in Subtyping]
has_type [in Norm]
has_type [in Stlc]
hoare_proof [in HoareAsLogic]

I

id [in ImpList]
id [in SfLib]
Id.id [in Imp]
instantiation [in Norm]

L

le [in Logic]
LeFirstTry.le [in Logic]
list [in Poly]
Loop.ceval_count [in PE]
Loop.pe_ceval_count [in PE]
Loop.pe_com [in PE]
ltac_Mark [in LibTactics]
ltac_No_arg [in LibTactics]
ltac_Wild [in LibTactics]
ltac_Wilds [in LibTactics]

M

MumbleBaz.baz [in Poly]
MumbleBaz.grumble [in Poly]
MumbleBaz.mumble [in Poly]
MyEquality.eq [in Logic]
MyEquality.eq' [in Logic]
MyProp [in Ind]

N

natlist [in Ind]
NatList.natlist [in Lists]
NatList.natoption [in Lists]
NatList.natprod [in Lists]
natlist1 [in Ind]
next_even [in Logic]
next_nat [in Logic]
next_nat [in SfLib]
nostutter [in Logic]
no_whilesR [in Imp]
nvalue [in Stlc]

O

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

P

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

R

record_tm [in RecordSub]
record_ty [in RecordSub]
refl_step_closure [in Rel]
refl_step_closure [in SfLib]
RepeatExercise.ceval [in Hoare]
RepeatExercise.com [in Hoare]
repeats [in Logic]
rgb [in Ind]
R.R [in Logic]

S

T

Temp1.step [in Smallstep]
Temp1.value [in Smallstep]
Temp2.step [in Smallstep]
Temp2.value [in Smallstep]
Temp3.step [in Smallstep]
Temp3.value [in Smallstep]
Temp4.step [in Smallstep]
Temp4.Temp5.step [in Smallstep]
Temp4.tm [in Smallstep]
Temp4.value [in Smallstep]
tm [in Norm]
tm [in Smallstep]
tm [in RecordSub]
tm [in Stlc]
tm [in Subtyping]
tm [in Subtyping]
total_relation [in SfLib]
tree [in Ind]
ty [in Subtyping]
ty [in Subtyping]
ty [in RecordSub]
ty [in Norm]
ty [in Stlc]

V

val [in ImpList]
value [in Smallstep]
value [in RecordSub]
value [in Norm]
value [in Subtyping]
value [in Subtyping]
var_not_used_in_aexp [in Equiv]

W

well_formed_ty [in RecordSub]

Y

yesno [in Ind]

Definition Index

A

add_slowly [in Hoare]
admit [in SfLib]
admit [in Basics]
aequiv [in Equiv]
aeval [in ImpList]
aeval [in Imp]
AExp.aeval [in Imp]
AExp.beval [in Imp]
AExp.optimize_0plus [in Imp]
AExp.silly_presburger_example [in Imp]
AExp.test_aeval1 [in Imp]
AExp.test_optimize_0plus [in Imp]
aexp1 [in Imp]
andb [in Basics]
andb3 [in Basics]
antisymmetric [in Rel]
app [in Poly]
app' [in Poly]
aslist [in ImpList]
asnat [in ImpList]
Assertion [in Hoare]
assert_implies [in Hoare]
assign [in PE]
assigned [in PE]
assn_sub [in Hoare]
assn_sub_example [in Hoare]
assn_sub_example' [in Hoare]
astep_example1 [in Stlc]
astep_example1' [in Stlc]
astep_example1'' [in Stlc]
astep_example1''' [in Stlc]
astep_many [in Stlc]
atrans_sound [in Equiv]

B

bassn [in Hoare]
bequiv [in Equiv]
beq_id [in ImpList]
beq_id [in SfLib]
beq_nat [in Basics]
beq_nat_sym [in Lists]
between [in Ind]
beval [in ImpList]
beval [in Imp]
bexp1 [in Imp]
ble_nat [in Basics]
ble_nat [in SfLib]
blt_nat [in Basics]
btrans_sound [in Equiv]
build_symtable [in ImpParser]

C

cequiv [in Equiv]
cequiv' [in Equiv]
ceval_example1 [in Imp]
ceval_example2 [in Imp]
ceval_step [in Imp]
ceval_step1 [in Imp]
ceval_step2 [in Imp]
ceval_step3 [in Imp]
CImp.cstepmany [in Smallstep]
CImp.par_loop [in Smallstep]
CImp.par_loop_example_0 [in Smallstep]
CImp.par_loop_example_2 [in Smallstep]
classic [in Logic]
classifyChar [in ImpParser]
closed [in Norm]
closed_env [in Norm]
combine [in Poly]
combine' [in Poly]
congruence_example [in Equiv]
conj_fact [in Logic]
constfun [in Poly]
constfun_example1 [in Poly]
constfun_example2 [in Poly]
context [in RecordSub]
context [in Subtyping]
context [in Subtyping]
context [in Norm]
countoddmembers' [in Poly]
ctrans_sound [in Equiv]

D

dec_correct [in Hoare]
dec_while [in Hoare]
de_morgan_not_and_not [in Logic]
Dictionary.find [in Lists]
Dictionary.insert [in Lists]
doit3times [in Poly]
double [in Basics]
drop [in Norm]

E

F

factorial [in Basics]
Factorial.fact_body [in Hoare]
Factorial.fact_com [in Hoare]
Factorial.fact_loop [in Hoare]
Factorial.real_fact [in Hoare]
fact_body [in Imp]
fact_com [in Imp]
fact_invariant [in Imp]
fact_in_coq [in Imp]
fact_loop [in Imp]
fdfs_wed' [in Ind]
filter [in Poly]
filter_even_gt7 [in Poly]
find_parity [in Hoare]
find_parity_invariant [in Hoare]
find_parity_invariant' [in Hoare]
firstExpect [in ImpParser]
flat_map [in Poly]
fmostlytrue [in Poly]
fold [in Poly]
fold_aexp_ex1 [in Equiv]
fold_aexp_ex2 [in Equiv]
fold_bexp_ex1 [in Equiv]
fold_bexp_ex2 [in Equiv]
fold_com_ex1 [in Equiv]
fold_constants_aexp [in Equiv]
fold_constants_bexp [in Equiv]
fold_constants_com [in Equiv]
fold_example1 [in Poly]
fold_example2 [in Poly]
fold_example3 [in Poly]
fold_length [in Poly]
fold_map [in Poly]
forallb [in Logic]
four_ev [in Ind]
fst [in Poly]
ftrue [in Poly]
funny_prop1 [in Logic]
funny_prop1' [in Logic]
funny_prop1'' [in Logic]

H

halts [in Norm]
has_type_not [in Stlc]
has_type_1 [in Stlc]
hd_opt [in Poly]
head [in ImpList]
hoare_asgn_example1 [in Hoare]
hoare_asgn_example1' [in Hoare]
hoare_asgn_example3 [in Hoare]
hoare_asgn_example4 [in Hoare]
hoare_triple [in Hoare]

I

identity_assignment' [in Equiv]
Id.beq_id [in Imp]
iff [in Logic]
if_example [in Hoare]
implies_to_or [in Logic]
index [in Poly]
InvertsExamples.typing_nonexample_1 [in UseTactics]
isAlpha [in ImpParser]
isDigit [in ImpParser]
isLowerAlpha [in ImpParser]
isWhite [in ImpParser]

K

keval [in PE]
keval_example [in PE]

L

length [in Poly]
length' [in Poly]
length'' [in Poly]
length_is_1 [in Poly]
list123 [in Poly]
list123' [in Poly]
list123'' [in Poly]
list123''' [in Poly]
list_member [in Hoare]
list_member_dec [in Hoare]
list_member_spec [in Hoare]
list_of_string [in ImpParser]
lookup [in Norm]
loop [in ImpList]
loop [in Imp]
Loop.pe_loop_example1 [in PE]
Loop.pe_loop_example2 [in PE]
Loop.pe_loop_example3 [in PE]
Loop.pe_loop_example4 [in PE]
Loop.square_loop [in PE]
lt [in Logic]
ltac_database [in LibTactics]
ltac_nat_from_int [in LibTactics]
ltac_something [in LibTactics]
ltac_tag_subst [in LibTactics]
ltac_to_generalize [in LibTactics]

M

many [in ImpParser]
many_helper [in ImpParser]
map [in Poly]
mextend [in Norm]
minustwo [in Basics]
msubst [in Norm]
MyEquality.four [in Logic]
MyEquality.singleton [in Logic]
myFact [in UseAuto]
mynil [in Poly]
mynil' [in Poly]
MyProp_iff_ev [in Logic]

N

O

oddb [in Basics]
okdw [in Ind]
okd_before2 [in Ind]
okd_before2_valid' [in Ind]
option_map [in Poly]
orb [in Basics]
order [in Rel]
our_nat_induction [in Ind]
override [in Poly]
override_example1 [in Poly]
override_example2 [in Poly]
override_example3 [in Poly]
override_example4 [in Poly]

P

p [in Logic]
parity [in PE]
parity_body [in PE]
parity_eval [in PE]
parse [in ImpParser]
parseAExp [in ImpParser]
parseAtomicExp [in ImpParser]
parseBExp [in ImpParser]
parseConjunctionExp [in ImpParser]
parseIdentifier [in ImpParser]
parseNumber [in ImpParser]
parsePrimaryExp [in ImpParser]
parseProductExp [in ImpParser]
parser [in ImpParser]
parseSequencedCommand [in ImpParser]
parseSimpleCommand [in ImpParser]
parseSumExp [in ImpParser]
partial_function [in Rel]
partial_function [in SfLib]
partial_map [in SfLib]
partition [in Poly]
peirce [in Logic]
pe_add [in PE]
pe_aexp [in PE]
pe_bexp [in PE]
pe_block [in PE]
pe_block_example [in PE]
pe_compare [in PE]
pe_consistent [in PE]
pe_disagree_at [in PE]
pe_example1 [in PE]
pe_example2 [in PE]
pe_example3 [in PE]
pe_lookup [in PE]
pe_override [in PE]
pe_program [in PE]
pe_remove [in PE]
pe_removes [in PE]
pe_state [in PE]
pe_unique [in PE]
Playground1.pred [in Basics]
Playground2.minus [in Basics]
Playground2.mult [in Basics]
Playground2.plus [in Basics]
plus2 [in Imp]
plus3 [in Poly]
plus_fact [in Ind]
post [in Hoare]
pre [in Hoare]
preorder [in Rel]
preserved_by_S [in Ind]
prod_curry [in Poly]
prod_uncurry [in Poly]
program [in PE]
pup_to_n [in Imp]
P_m0r [in Ind]
P_m0r' [in Ind]

R

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

S

T

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

U

update [in Imp]
update [in ImpList]

V

value [in Stlc]
verification_conditions [in Hoare]

W

while_example [in Hoare]

X

X [in Imp]
X [in ImpList]
XtimesYinZ [in Imp]

Y

Y [in ImpList]
Y [in Imp]

Z

Z [in ImpList]
Z [in Imp]

Module Index

A

aevalR_first_try [in Imp]
AExp [in Imp]

C

CasesExample [in UseTactics]
CImp [in Smallstep]
Combined [in Smallstep]
Context [in Stlc]

D

DeterministicImp [in UseAuto]
Dictionary [in Lists]

E

EqualityExamples [in UseTactics]
Examples [in Subtyping]
Examples [in Subtyping]
Examples [in RecordSub]
Examples [in MoreStlc]
ExamplesInstantiations [in UseTactics]
ExamplesLets [in UseTactics]
Examples2 [in Subtyping]
Examples2 [in Subtyping]
Examples2 [in RecordSub]
ExampleVariables [in References]

F

Factorial [in Hoare]
FirstTry [in Records]
FixTest1 [in MoreStlc]
FixTest2 [in MoreStlc]
FixTest3 [in MoreStlc]
FixTest4 [in MoreStlc]

G

GenExample [in UseTactics]

I

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

L

LeFirstTry [in Logic]
LetTest [in MoreStlc]
LibTacticsCompatibility [in LibTactics]
ListTest [in MoreStlc]
Loop [in PE]

M

MumbleBaz [in Poly]
MyEquality [in Logic]

N

NaryExamples [in UseTactics]
NatList [in Lists]
Numtest [in MoreStlc]

P

P [in Ind]
Playground1 [in Basics]
Playground2 [in Basics]
PreservationProgressReferences [in UseAuto]
PreservationProgressStlc [in UseAuto]
Prodtest [in MoreStlc]

R

R [in Logic]
RepeatExercise [in Hoare]
RingDemo [in UseAuto]

S

Semantics [in UseAuto]
SimpleArith0 [in Smallstep]
SimpleArith1 [in Smallstep]
SimpleArith2 [in Smallstep]
SkipExample [in UseTactics]
SortExamples [in UseTactics]
STLC [in Stlc]
STLCArith [in Stlc]
STLCChecker [in Typechecking]
STLCExtended [in MoreStlc]
STLCExtendedRecords [in Records]
STLCRef [in References]
SubtypingInversion [in UseAuto]
Sumtest1 [in MoreStlc]
Sumtest2 [in MoreStlc]

T

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

U

UnfoldsExample [in UseTactics]

Axiom Index

E

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

F

functional_extensionality [in Equiv]

G

gt_not_le [in UseAuto]

I

inj_pair2 [in LibTactics]

L

le_gt_false [in UseAuto]
le_not_gt [in UseAuto]

P

P [in UseAuto]

S

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

T

typ [in UseAuto]

Variable Index

E

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

S

skip_axiom [in LibTactics]

Library Index

B

Basics

E

Equiv

H

Hoare
HoareAsLogic

I

Imp
ImpList
ImpParser
Ind

L

LibTactics
Lists
Logic

M

MoreStlc

N

Norm

P

PE
Poly
Postscript
Preface

R

Records
RecordSub
References
Rel

S

SfLib
Smallstep
Stlc
Subtyping
Subtyping
Symbols

T

Typechecking

U

UseAuto
UseTactics

Global Index

(2463 entries)

Lemma Index

(710 entries)

Section Index

(4 entries)

Constructor Index

(768 entries)

Abbreviation Index

(66 entries)

Inductive Index

(186 entries)

Definition Index

(610 entries)

Module Index

(69 entries)

Axiom Index

(12 entries)

Variable Index

(8 entries)

Library Index

(30 entries)

This page has been generated by coqdoc