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 _ other (1484 entries)
Projection 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 _ other (7 entries)
Record 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 _ other (3 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 _ other (354 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 _ other (77 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 _ other (245 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 _ other (33 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 _ other (99 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 _ other (385 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 _ other (14 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 _ other (16 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 _ other (233 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 _ other (18 entries)

Global Index

A

Abs [constructor, in Abs]
Abs [constructor, in Abs]
Abs [constructor, in Abs]
Acc_intro' [definition, in Acc_intro']
add [definition, in add]
addLists [definition, in addLists]
addLists' [definition, in addLists']
All [definition, in All]
All [section, in All]
allTrue [definition, in allTrue]
allTrue_add [lemma, in allTrue_add]
allTrue_In [lemma, in allTrue_In]
All.P [variable, in P]
All.T [variable, in T]
And [constructor, in And]
And [constructor, in And]
And [constructor, in And]
And [constructor, in And]
And [constructor, in And]
And [constructor, in And]
and [inductive, in and]
and_assoc [lemma, in and_assoc]
and_True_prem [lemma, in and_True_prem]
and_True_conc [lemma, in and_True_conc]
and_comm [lemma, in and_comm]
And' [constructor, in And']
And' [constructor, in And']
Answer [constructor, in Answer]
App [constructor, in App]
App [constructor, in App]
app [definition, in app]
app [definition, in app]
app [definition, in app]
append_emp [lemma, in append_emp]
append' [definition, in append']
approx [definition, in approx]
app_cong [lemma, in app_cong]
app_empty_end [lemma, in app_empty_end]
app' [definition, in app']
arith_neq' [lemma, in arith_neq']
arith_comm [lemma, in arith_comm]
arith_comm' [lemma, in arith_comm']
arith_neq [lemma, in arith_neq]
Arrow [constructor, in Arrow]
asgn [definition, in asgn]
Assign [constructor, in Assign]
associativity [lemma, in associativity]
Atomic [constructor, in Atomic]
Atomic' [constructor, in Atomic']
autorewrite [section, in autorewrite]
autorewrite.A [variable, in A]
autorewrite.f [variable, in f]
autorewrite.f_f [variable, in f_f]
autorewrite.garden_path.P [variable, in P]
autorewrite.garden_path.P [variable, in P]
autorewrite.garden_path.g [variable, in g]
autorewrite.garden_path.g [variable, in g]
autorewrite.garden_path.g [variable, in g]
autorewrite.garden_path [section, in garden_path]
autorewrite.garden_path [section, in garden_path]
autorewrite.garden_path [section, in garden_path]
autorewrite.garden_path.f_g [variable, in f_g]
autorewrite.garden_path.f_g [variable, in f_g]
autorewrite.garden_path.f_g [variable, in f_g]
a_b [definition, in a_b]
a_star [definition, in a_star]


B

backward [definition, in backward]
bad [definition, in bad]
balanced [lemma, in balanced]
balance1 [definition, in balance1]
balance2 [definition, in balance2]
Bar [constructor, in Bar]
bar [inductive, in bar]
bar [definition, in bar]
Base [constructor, in Base]
BConst [constructor, in BConst]
BConst [constructor, in BConst]
Bind [definition, in Bind]
Bind [section, in Bind]
Bind.A [variable, in A]
Bind.B [variable, in B]
Bind.m1 [variable, in m1]
Bind.m2 [variable, in m2]
Binop [constructor, in Binop]
binop [inductive, in binop]
binopDenote [definition, in binopDenote]
Black [constructor, in Black]
BlackNode [constructor, in BlackNode]
bleh [definition, in bleh]
Bnd [constructor, in Bnd]
Bool [constructor, in Bool]
Bool [constructor, in Bool]
Bool [constructor, in Bool]
Bool [constructor, in Bool]
bool [inductive, in bool]
bool [inductive, in bool]
bool_den [definition, in bool_den]
bool_neq [lemma, in bool_neq]
bool_neq [lemma, in bool_neq]
bool_fix [definition, in bool_fix]
bool_dt [definition, in bool_dt]
boool [definition, in boool]
Bottom [definition, in Bottom]
Bottom [section, in Bottom]
Bottom.A [variable, in A]


C

cassociativity [lemma, in cassociativity]
cassociativity1 [lemma, in cassociativity1]
cassociativity2 [lemma, in cassociativity2]
cast [definition, in cast]
cfold [definition, in cfold]
cfold [definition, in cfold]
cfoldCond [definition, in cfoldCond]
cfoldCond [section, in cfoldCond]
cfoldCond_correct [lemma, in cfoldCond_correct]
cfoldCond.default [variable, in default]
cfoldCond.t [variable, in t]
cfold_correct [lemma, in cfold_correct]
cfold_correct [lemma, in cfold_correct]
cfold_correct [lemma, in cfold_correct]
cfold_correct [lemma, in cfold_correct]
cfold_correct [lemma, in cfold_correct]
ChainCons [constructor, in ChainCons]
Char [constructor, in Char]
check_even [definition, in check_even]
choice_Set [definition, in choice_Set]
classic [axiom, in classic]
cleft_identity [lemma, in cleft_identity]
Client [module, in Client]
Client.D [module, in Client.D]
Client.E [module, in Client.E]
cmd [inductive, in cmd]
Coinductive [library]
color [inductive, in color]
combine [lemma, in combine]
comm_conc [lemma, in comm_conc]
comm_prem [lemma, in comm_prem]
comp [inductive, in comp]
compile [definition, in compile]
compile_correct [lemma, in compile_correct]
compile_correct [lemma, in compile_correct]
compile_correct' [lemma, in compile_correct']
compile_correct' [lemma, in compile_correct']
computation [definition, in computation]
computation [section, in computation]
computation.A [variable, in A]
comp_eq [definition, in comp_eq]
Con [constructor, in Con]
Concat [constructor, in Concat]
Conclusion [library]
Cond [constructor, in Cond]
cond [definition, in cond]
cond [section, in cond]
cond_ext [lemma, in cond_ext]
cond.A [variable, in A]
cond.default [variable, in default]
confounder [lemma, in confounder]
conj [constructor, in conj]
Conjunction [constructor, in Conjunction]
conj' [definition, in conj']
Cons [constructor, in Cons]
Cons [constructor, in Cons]
Cons [constructor, in Cons]
Cons [constructor, in Cons]
Cons [constructor, in Cons]
Const [constructor, in Const]
Const [constructor, in Const]
Const [constructor, in Const]
Const [constructor, in Const]
Const [constructor, in Const]
Const [constructor, in Const]
Const [constructor, in Const]
Const [constructor, in Const]
ConstP [constructor, in ConstP]
constructor [record, in constructor]
constructorDenote [definition, in constructorDenote]
contra [lemma, in contra]
copies [definition, in copies]
cright_identity [lemma, in cright_identity]
curriedAdd [definition, in curriedAdd]
curriedAdd' [definition, in curriedAdd']


D

DataStruct [library]
datatype [definition, in datatype]
datatypeDenote [definition, in datatypeDenote]
datatypeDenoteOk [definition, in datatypeDenoteOk]
dec_star' [definition, in dec_star']
dec_star'' [definition, in dec_star'']
dec_star.dec_star'' [section, in dec_star'']
dec_star.P [variable, in P]
dec_star.dec_star''.n [variable, in n]
dec_star.s [variable, in s]
dec_star [definition, in dec_star]
dec_star [section, in dec_star]
dec_star.P_dec [variable, in P_dec]
dec_star.dec_star''.P'_dec [variable, in P'_dec]
dec_star.dec_star''.P' [variable, in P']
deeeebug [definition, in deeeebug]
denote [section, in denote]
denote.T [variable, in T]
depth [definition, in depth]
depth [section, in depth]
depth_max' [lemma, in depth_max']
depth_max [lemma, in depth_max]
depth_max [lemma, in depth_max]
depth_min [lemma, in depth_min]
depth.f [variable, in f]
doublePred [definition, in doublePred]
doublePred' [definition, in doublePred']


E

eapp [definition, in eapp]
ECons [constructor, in ECons]
eir [definition, in eir]
elength [definition, in elength]
elength_eapp [lemma, in elength_eapp]
elength_eapp [lemma, in elength_eapp]
Empty [constructor, in Empty]
Empty_set_fix [definition, in Empty_set_fix]
Empty_set [inductive, in Empty_set]
Empty_set [inductive, in Empty_set]
Empty_set_den [definition, in Empty_set_den]
Empty_set_dt [definition, in Empty_set_dt]
ENil [constructor, in ENil]
eq [inductive, in eq]
Eq [constructor, in Eq]
Eq [constructor, in Eq]
Eq [constructor, in Eq]
Eq [constructor, in Eq]
EqAnswer [constructor, in EqAnswer]
EqP [constructor, in EqP]
eqPlus [inductive, in eqPlus]
EqThinkL [constructor, in EqThinkL]
EqThinkR [constructor, in EqThinkR]
Equality [library]
eq_type_dec [definition, in eq_type_dec]
eq_nat_dec' [definition, in eq_nat_dec']
eq_refl [constructor, in eq_refl]
eq_nat_dec [definition, in eq_nat_dec]
er [definition, in er]
eval [definition, in eval]
eval [definition, in eval]
eval [inductive, in eval]
eval [inductive, in eval]
EvalAnswer [constructor, in EvalAnswer]
EvalAssign [constructor, in EvalAssign]
evalCmd [inductive, in evalCmd]
evalCmd_coind.R [variable, in R]
evalCmd_coind.SeqCase [variable, in SeqCase]
evalCmd_coind [lemma, in evalCmd_coind]
evalCmd_coind [section, in evalCmd_coind]
evalCmd_coind.AssignCase [variable, in AssignCase]
evalCmd_coind.WhileCase [variable, in WhileCase]
EvalConst [constructor, in EvalConst]
EvalConst' [lemma, in EvalConst']
evalExp [definition, in evalExp]
EvalPlus [constructor, in EvalPlus]
EvalPlus' [lemma, in EvalPlus']
EvalSeq [constructor, in EvalSeq]
EvalThink [constructor, in EvalThink]
EvalVar [constructor, in EvalVar]
EvalVar' [lemma, in EvalVar']
EvalWhileFalse [constructor, in EvalWhileFalse]
EvalWhileTrue [constructor, in EvalWhileTrue]
eval_fact [lemma, in eval_fact]
eval_frob [lemma, in eval_frob]
eval_times [lemma, in eval_times]
eval_times [lemma, in eval_times]
eval_times [lemma, in eval_times]
eval_times [lemma, in eval_times]
eval_times [lemma, in eval_times]
eval_times [lemma, in eval_times]
eval_times [lemma, in eval_times]
eval_times [lemma, in eval_times]
eval1 [definition, in eval1]
eval1' [definition, in eval1']
eval1' [definition, in eval1']
even [inductive, in even]
EvenO [constructor, in EvenO]
EvenSS [constructor, in EvenSS]
even_1_contra [lemma, in even_1_contra]
even_list_mut'.Podd [variable, in Podd]
even_list_mut [definition, in even_list_mut]
even_4' [lemma, in even_4']
Even_SS [constructor, in Even_SS]
even_plus [lemma, in even_plus]
even_256' [lemma, in even_256']
even_list_mut'.ECons_case [variable, in ECons_case]
even_255 [lemma, in even_255]
even_256 [lemma, in even_256]
even_list_mut'.OCons_case [variable, in OCons_case]
even_contra' [lemma, in even_contra']
even_3_contra [lemma, in even_3_contra]
even_0 [lemma, in even_0]
even_4 [lemma, in even_4]
even_list_mut' [definition, in even_list_mut']
even_list_mut' [section, in even_list_mut']
Even_O [constructor, in Even_O]
even_list_mut'.Peven [variable, in Peven]
even_contra [lemma, in even_contra]
even_contra [lemma, in even_contra]
even_contra'' [lemma, in even_contra'']
even_list_mut'.ENil_case [variable, in ENil_case]
even_list [inductive, in even_list]
evilStream [inductive, in evilStream]
ex [inductive, in ex]
exec [inductive, in exec]
ExecBnd [constructor, in ExecBnd]
ExecRet [constructor, in ExecRet]
exec_frob [lemma, in exec_frob]
existT' [definition, in existT']
exist1 [lemma, in exist1]
exist2 [lemma, in exist2]
exp [inductive, in exp]
exp [inductive, in exp]
exp [inductive, in exp]
exp [inductive, in exp]
exp [inductive, in exp]
exp [inductive, in exp]
exp [inductive, in exp]
exp [inductive, in exp]
exp [inductive, in exp]
expDenote [definition, in expDenote]
expDenote [definition, in expDenote]
expDenote [definition, in expDenote]
expP [inductive, in expP]
exp' [inductive, in exp']
exp'Denote [definition, in exp'Denote]
exp'Denote [definition, in exp'Denote]
ex_intro [constructor, in ex_intro]
ex_irrelevant [lemma, in ex_irrelevant]
ex_prem [lemma, in ex_prem]
ex_conc [lemma, in ex_conc]
ex_symmetry [lemma, in ex_symmetry]
ex1 [definition, in ex1]
e2u [definition, in e2u]


F

fact [definition, in fact]
fact_iter' [definition, in fact_iter']
fact_def [lemma, in fact_def]
fact_slow' [definition, in fact_slow']
fact_eq [lemma, in fact_eq]
fact_eq' [lemma, in fact_eq']
fact_iter [definition, in fact_iter]
fact_eq'' [lemma, in fact_eq'']
fact_slow [definition, in fact_slow]
Fals [constructor, in Fals]
false [constructor, in false]
false [constructor, in false]
falseFree [inductive, in falseFree]
falseFree_holds [lemma, in falseFree_holds]
Falsehood [constructor, in Falsehood]
Falsehood [constructor, in Falsehood]
Falsehood' [constructor, in Falsehood']
falses_trues [definition, in falses_trues]
False_imp [lemma, in False_imp]
False_prem [lemma, in False_prem]
False' [definition, in False']
FFAnd [constructor, in FFAnd]
ffin [definition, in ffin]
FFNot [constructor, in FFNot]
FFTru [constructor, in FFTru]
fget [definition, in fget]
fhapp [definition, in fhapp]
fhapp [section, in fhapp]
fhapp_assoc'' [lemma, in fhapp_assoc'']
fhapp_assoc' [lemma, in fhapp_assoc']
fhapp_assoc [lemma, in fhapp_assoc]
fhapp' [section, in fhapp']
fhapp'' [section, in fhapp'']
fhapp''.A [variable, in A]
fhapp''.B [variable, in B]
fhapp'.A [variable, in A]
fhapp'.B [variable, in B]
fhapp.A [variable, in A]
fhapp.B [variable, in B]
fhget [definition, in fhget]
fhget [definition, in fhget]
fhget_fhmap [lemma, in fhget_fhmap]
fhlist [definition, in fhlist]
fhlist [section, in fhlist]
fhlist [definition, in fhlist]
fhlist [section, in fhlist]
fhlist_map.A [variable, in A]
fhlist_map.B [variable, in B]
fhlist_map.C [variable, in C]
fhlist_map.f [variable, in f]
fhlist_map.elm [variable, in elm]
fhlist_map [section, in fhlist_map]
fhlist.A [variable, in A]
fhlist.A [variable, in A]
fhlist.B [variable, in B]
fhlist.B [variable, in B]
fhlist.elm [variable, in elm]
fhlist.elm [variable, in elm]
fhmap [definition, in fhmap]
fi [definition, in fi]
fib [definition, in fib]
filist [definition, in filist]
filist [section, in filist]
filist.A [variable, in A]
filter [definition, in filter]
fin [inductive, in fin]
finOut [definition, in finOut]
fin_cases [lemma, in fin_cases]
fin_cases_again [lemma, in fin_cases_again]
fin_cases_again' [lemma, in fin_cases_again']
First [constructor, in First]
FirstOrder [module, in FirstOrder]
firstorder [section, in firstorder]
firstorder' [section, in firstorder']
firstorder'.A [variable, in A]
firstorder'.H1 [variable, in H1]
firstorder'.H2 [variable, in H2]
firstorder'.P [variable, in P]
firstorder'.Q [variable, in Q]
firstorder'.R [variable, in R]
firstorder'.S [variable, in S]
firstorder.A [variable, in A]
FirstOrder.Abs [constructor, in Abs]
FirstOrder.add [definition, in add]
FirstOrder.App [constructor, in App]
FirstOrder.cfold [definition, in cfold]
FirstOrder.cfoldSound [lemma, in cfoldSound]
FirstOrder.Const [constructor, in Const]
firstorder.H1 [variable, in H1]
firstorder.H2 [variable, in H2]
FirstOrder.ident [definition, in ident]
FirstOrder.identSound [lemma, in identSound]
FirstOrder.insertAt [definition, in insertAt]
FirstOrder.insertAtS [definition, in insertAtS]
FirstOrder.Let [constructor, in Let]
FirstOrder.lift [definition, in lift]
FirstOrder.liftSound [lemma, in liftSound]
FirstOrder.liftVar [definition, in liftVar]
FirstOrder.liftVarSound [lemma, in liftVarSound]
FirstOrder.lift' [definition, in lift']
FirstOrder.lift'Sound [lemma, in lift'Sound]
firstorder.P [variable, in P]
FirstOrder.Plus [constructor, in Plus]
firstorder.Q [variable, in Q]
firstorder.R [variable, in R]
firstorder.S [variable, in S]
FirstOrder.term [inductive, in term]
FirstOrder.termDenote [definition, in termDenote]
FirstOrder.three_the_hard_way [definition, in three_the_hard_way]
FirstOrder.unlet [definition, in unlet]
FirstOrder.unletSound [lemma, in unletSound]
FirstOrder.unletSound' [lemma, in unletSound']
FirstOrder.Var [constructor, in Var]
five_plus_three [definition, in five_plus_three]
Fix [definition, in Fix]
Fix [section, in Fix]
fixDenote [definition, in fixDenote]
fixDenoteOk [definition, in fixDenoteOk]
Fix' [definition, in Fix']
Fix'_ok [lemma, in Fix'_ok]
Fix.A [variable, in A]
Fix.B [variable, in B]
Fix.f [variable, in f]
Fix.f_continuous [variable, in f_continuous]
flatten [definition, in flatten]
flatten_correct' [lemma, in flatten_correct']
flatten_correct [lemma, in flatten_correct]
fmember [definition, in fmember]
fmember [definition, in fmember]
fo [lemma, in fo]
foldr_plus [lemma, in foldr_plus]
Foo [constructor, in Foo]
foo [inductive, in foo]
foo [definition, in foo]
foo [definition, in foo]
foo [definition, in foo]
foo [definition, in foo]
Forall [section, in Forall]
Forall [constructor, in Forall]
Forall [constructor, in Forall]
forall_and.both [variable, in both]
forall_and.A [variable, in A]
forall_and.P [variable, in P]
forall_and.Q [variable, in Q]
Forall_weaken [lemma, in Forall_weaken]
forall_exists_commute [lemma, in forall_exists_commute]
Forall_In' [lemma, in Forall_In']
Forall_c [definition, in Forall_c]
forall_refl [definition, in forall_refl]
forall_eq [lemma, in forall_eq]
Forall_In [lemma, in Forall_In]
forall_and [lemma, in forall_and]
forall_and [section, in forall_and]
Forall.A [variable, in A]
Forall.P [variable, in P]
Forall.P' [variable, in P']
formula [inductive, in formula]
formula [inductive, in formula]
formula [inductive, in formula]
formulaDenote [definition, in formulaDenote]
formulaDenote [definition, in formulaDenote]
formula_ind'.P [variable, in P]
formula_ind'.Eq_case [variable, in Eq_case]
formula_ind' [definition, in formula_ind']
formula_ind' [section, in formula_ind']
formula_ind'.And_case [variable, in And_case]
formula_ind'.Forall_case [variable, in Forall_case]
formula' [inductive, in formula']
forward [definition, in forward]
Found [constructor, in Found]
four_plus_three [definition, in four_plus_three]
four_plus_three' [definition, in four_plus_three']
fo' [lemma, in fo']
frob [definition, in frob]
frob [definition, in frob]
frob_eq [lemma, in frob_eq]
frob_eq [lemma, in frob_eq]
frob' [definition, in frob']
from_one_to_zero [definition, in from_one_to_zero]
Fst [constructor, in Fst]
Func [constructor, in Func]
Func [constructor, in Func]
f_f_f_g [lemma, in f_f_f_g]
f_f_f [lemma, in f_f_f]
f_f_f' [lemma, in f_f_f']
f_f_f' [lemma, in f_f_f']
f_f_f' [lemma, in f_f_f']


G

GeneralRec [library]
Generic [library]
get [definition, in get]
get [definition, in get]
getNat [definition, in getNat]
getNat_is_reasonable [lemma, in getNat_is_reasonable]
getNat_is_reasonable [lemma, in getNat_is_reasonable]
getNat' [definition, in getNat']
get_imap [lemma, in get_imap]
ge_refl [lemma, in ge_refl]
GROUP [module, in GROUP]
GroupProofs [module, in GroupProofs]
GroupProofs.ident' [lemma, in ident']
GroupProofs.inverse' [lemma, in inverse']
GroupProofs.M [module, in GroupProofs.M]
GroupProofs.unique_ident [lemma, in unique_ident]
GROUP_THEOREMS.M [module, in GROUP_THEOREMS.M]
GROUP_THEOREMS.inverse' [axiom, in inverse']
GROUP_THEOREMS.ident' [axiom, in ident']
GROUP_THEOREMS [module, in GROUP_THEOREMS]
GROUP_THEOREMS.unique_ident [axiom, in unique_ident]
GROUP.assoc [axiom, in assoc]
GROUP.f [axiom, in f]
GROUP.G [axiom, in G]
GROUP.i [axiom, in i]
GROUP.id [axiom, in id]
GROUP.ident [axiom, in ident]
GROUP.inverse [axiom, in inverse]


H

HAnd [constructor, in HAnd]
HAnd' [constructor, in HAnd']
hasType [inductive, in hasType]
hasType_det [lemma, in hasType_det]
HCons [constructor, in HCons]
hd [definition, in hd]
hd [definition, in hd]
hd' [definition, in hd']
HFirst [constructor, in HFirst]
hget [definition, in hget]
hi [definition, in hi]
HigherOrder [module, in HigherOrder]
HigherOrder.Abs [constructor, in Abs]
HigherOrder.Add [definition, in Add]
HigherOrder.add [definition, in add]
HigherOrder.add' [definition, in add']
HigherOrder.App [constructor, in App]
HigherOrder.Cfold [definition, in Cfold]
HigherOrder.cfold [definition, in cfold]
HigherOrder.CfoldSound [lemma, in CfoldSound]
HigherOrder.cfoldSound [lemma, in cfoldSound]
HigherOrder.Const [constructor, in Const]
HigherOrder.countVars [definition, in countVars]
HigherOrder.CountVars [definition, in CountVars]
HigherOrder.First [projection, in First]
HigherOrder.Ident [definition, in Ident]
HigherOrder.ident [definition, in ident]
HigherOrder.IdentSound [lemma, in IdentSound]
HigherOrder.identSound [lemma, in identSound]
HigherOrder.Let [constructor, in Let]
HigherOrder.Plus [constructor, in Plus]
HigherOrder.pretty [definition, in pretty]
HigherOrder.Pretty [definition, in Pretty]
HigherOrder.Second [projection, in Second]
HigherOrder.squash [definition, in squash]
HigherOrder.Subst [definition, in Subst]
HigherOrder.Term [definition, in Term]
HigherOrder.term [inductive, in term]
HigherOrder.TermDenote [definition, in TermDenote]
HigherOrder.termDenote [definition, in termDenote]
HigherOrder.Term1 [definition, in Term1]
HigherOrder.three_the_hard_way [definition, in three_the_hard_way]
HigherOrder.three_the_hard_way' [definition, in three_the_hard_way']
HigherOrder.Three_the_hard_way [definition, in Three_the_hard_way]
HigherOrder.three_a_harder_way [definition, in three_a_harder_way]
HigherOrder.three_the_hard_way_Wf [lemma, in three_the_hard_way_Wf]
HigherOrder.Ty [projection, in Ty]
HigherOrder.unlet [definition, in unlet]
HigherOrder.Unlet [definition, in Unlet]
HigherOrder.UnletSound [lemma, in UnletSound]
HigherOrder.unletSound [lemma, in unletSound]
HigherOrder.unletWf [lemma, in unletWf]
HigherOrder.UnletWf [lemma, in UnletWf]
HigherOrder.Var [constructor, in Var]
HigherOrder.var [section, in var]
HigherOrder.varEntry [record, in varEntry]
HigherOrder.var.var [variable, in var]
HigherOrder.Wf [definition, in Wf]
HigherOrder.wf [inductive, in wf]
HigherOrder.wf [section, in wf]
HigherOrder.WfAbs [constructor, in WfAbs]
HigherOrder.WfApp [constructor, in WfApp]
HigherOrder.WfConst [constructor, in WfConst]
HigherOrder.WfLet [constructor, in WfLet]
HigherOrder.WfPlus [constructor, in WfPlus]
HigherOrder.WfVar [constructor, in WfVar]
HigherOrder.wf_monotone [lemma, in wf_monotone]
HigherOrder.wf.var1 [variable, in var1]
HigherOrder.wf.var2 [variable, in var2]
_ @ _ [notation, in ::x_'@'_x]
_ @+ _ [notation, in ::x_'@+'_x]
_ --> _ [notation, in ::x_'-->'_x]
# [notation, in ::'#']
[ _ ] [notation, in ::'['_x_']']
\ _ : _ , _ [notation, in ::'\'_x_':'_x_','_x]
^ [notation, in ::'^']
hlist [inductive, in hlist]
hlist [section, in hlist]
hlist.A [variable, in A]
hlist.B [variable, in B]
hlist.elm [variable, in elm]
hmap [section, in hmap]
hmap_hmap [lemma, in hmap_hmap]
hmap.A [variable, in A]
hmap.B1 [variable, in B1]
hmap.B2 [variable, in B2]
hmap.B3 [variable, in B3]
hmap.f1 [variable, in f1]
hmap.f2 [variable, in f2]
hmm [lemma, in hmm]
hmm' [lemma, in hmm']
hmm2 [lemma, in hmm2]
HNext [constructor, in HNext]
HNil [constructor, in HNil]
holds [definition, in holds]
holds [inductive, in holds]
holds' [inductive, in holds']
HOr1 [constructor, in HOr1]
HOr1' [constructor, in HOr1']
HOr2 [constructor, in HOr2]
HOr2' [constructor, in HOr2']
HtAnd [constructor, in HtAnd]
HtBool [constructor, in HtBool]
HtNat [constructor, in HtNat]
HtPlus [constructor, in HtPlus]
HTru [constructor, in HTru]
HTru' [constructor, in HTru']


I

iBinop [constructor, in iBinop]
iConst [constructor, in iConst]
id [definition, in id]
id [definition, in id]
id [definition, in id]
Ident [constructor, in Ident]
id' [definition, in id']
If [constructor, in If]
ifoldr [definition, in ifoldr]
ifoldr [section, in ifoldr]
ifoldr.A [variable, in A]
ifoldr.B [variable, in B]
ifoldr.f [variable, in f]
ifoldr.i [variable, in i]
ilist [definition, in ilist]
ilist [inductive, in ilist]
ilist [section, in ilist]
ilist [inductive, in ilist]
ilist [section, in ilist]
ilist_map.A [variable, in A]
ilist_map.B [variable, in B]
ilist_map.f [variable, in f]
ilist_map [section, in ilist_map]
ilist.A [variable, in A]
ilist.A [variable, in A]
illustrative_but_silly_detour [lemma, in illustrative_but_silly_detour]
illustrative_but_silly_detour [lemma, in illustrative_but_silly_detour]
imap [definition, in imap]
imap [definition, in imap]
Imp [constructor, in Imp]
imp [definition, in imp]
imp [definition, in imp]
imp_True [lemma, in imp_True]
Imp' [constructor, in Imp']
inc [definition, in inc]
inc [definition, in inc]
index_eq [definition, in index_eq]
InductiveTypes [library]
infiniteDecreasingChain [inductive, in infiniteDecreasingChain]
inject [definition, in inject]
Inject [constructor, in Inject]
inject_inverse [lemma, in inject_inverse]
ins [definition, in ins]
insert [definition, in insert]
insert [section, in insert]
insert [definition, in insert]
insertResult [definition, in insertResult]
insert.present [section, in present]
insert.present.z [variable, in z]
insert.x [variable, in x]
insResult [definition, in insResult]
instr [inductive, in instr]
instrDenote [definition, in instrDenote]
Int [module, in Int]
interleave [definition, in interleave]
interleave [section, in interleave]
interleave.A [variable, in A]
IntProofs [module, in IntProofs]
Intro [library]
Int.assoc [lemma, in assoc]
Int.f [definition, in f]
Int.G [definition, in G]
Int.i [definition, in i]
Int.id [definition, in id]
Int.ident [lemma, in ident]
Int.inverse [lemma, in inverse]
In_dec.A [variable, in A]
In_dec.A_eq_dec [variable, in A_eq_dec]
In_dec [definition, in In_dec]
In_dec [definition, in In_dec]
In_dec [section, in In_dec]
in_star [lemma, in in_star]
isEven [inductive, in isEven]
isZero [inductive, in isZero]
isZero [definition, in isZero]
IsZero [constructor, in IsZero]
isZero_contra' [lemma, in isZero_contra']
isZero_plus [lemma, in isZero_plus]
isZero_zero [lemma, in isZero_zero]
isZero_contra [lemma, in isZero_contra]
Iter [constructor, in Iter]


J

jme [definition, in jme]
JMeq_refl' [lemma, in JMeq_refl']
JMeq_eq' [lemma, in JMeq_eq']
JMeq' [definition, in JMeq']


L

Large [library]
lattice [section, in lattice]
lattice.A [variable, in A]
Leaf [constructor, in Leaf]
Leaf [constructor, in Leaf]
Leaf [constructor, in Leaf]
Leaf [constructor, in Leaf]
left_identity [lemma, in left_identity]
lemma1 [lemma, in lemma1]
lemma1' [definition, in lemma1']
lemma2 [definition, in lemma2]
lemma2 [lemma, in lemma2]
lemma3 [lemma, in lemma3]
lemma3 [lemma, in lemma3]
lemma3' [definition, in lemma3']
lemma4 [lemma, in lemma4]
length [definition, in length]
length [definition, in length]
lengthOrder [definition, in lengthOrder]
lengthOrder_wf [lemma, in lengthOrder_wf]
lengthOrder_wf' [lemma, in lengthOrder_wf']
length_is_2 [definition, in length_is_2]
length_is_2 [definition, in length_is_2]
length_1_2 [definition, in length_1_2]
length_emp [lemma, in length_emp]
length_and_sum [definition, in length_and_sum]
length_app [lemma, in length_app]
length_app [lemma, in length_app]
length_and_sum'' [definition, in length_and_sum'']
length_app1 [lemma, in length_app1]
length_and_sum' [definition, in length_and_sum']
length_O [lemma, in length_O]
length_S [lemma, in length_S]
leq [definition, in leq]
leq_Some [lemma, in leq_Some]
leq_None [lemma, in leq_None]
Lib [module, in Lib]
Lib.A [module, in Lib.A]
Lib.B [module, in Lib.B]
Lib.C [module, in Lib.C]
Lift [constructor, in Lift]
linear [lemma, in linear]
list [inductive, in list]
list [section, in list]
list [inductive, in list]
list_fix [definition, in list_fix]
list_nat_tree_ind [definition, in list_nat_tree_ind]
list_dt [definition, in list_dt]
list_den [definition, in list_den]
list.T [variable, in T]
LogicProg [library]
looper [definition, in looper]
looper [definition, in looper]


M

makeRbtree [definition, in makeRbtree]
map [definition, in map]
map [definition, in map]
map [definition, in map]
map [definition, in map]
map [section, in map]
map [definition, in map]
map [section, in map]
mapp [definition, in mapp]
map_nat [definition, in map_nat]
map_id [lemma, in map_id]
map' [definition, in map']
map' [section, in map']
map'.A [variable, in A]
map'.B [variable, in B]
map'.f [variable, in f]
map.A [variable, in A]
map.B [variable, in B]
map.F [variable, in F]
map.f [variable, in f]
map.T [variable, in T]
map.T' [variable, in T']
Match [lemma, in Match]
Match [library]
matches [definition, in matches]
max_spec_le [lemma, in max_spec_le]
max_1 [lemma, in max_1]
max_2 [lemma, in max_2]
maybe [inductive, in maybe]
mdenote [definition, in mdenote]
member [inductive, in member]
meq [definition, in meq]
merge [definition, in merge]
mergeSort [definition, in mergeSort]
mergeSort [section, in mergeSort]
mergeSort_eq [lemma, in mergeSort_eq]
mergeSort' [definition, in mergeSort']
mergeSort'' [definition, in mergeSort'']
mergeSort.A [variable, in A]
mergeSort.le [variable, in le]
mexp [inductive, in mexp]
minus_minus [lemma, in minus_minus]
mldenote [definition, in mldenote]
monoid [section, in monoid]
monoid_reflect [lemma, in monoid_reflect]
monoid.A [variable, in A]
monoid.assoc [variable, in assoc]
monoid.e [variable, in e]
monoid.f [variable, in f]
monoid.identl [variable, in identl]
monoid.identr [variable, in identr]
_ + _ [notation, in ::x_'+'_x]
MoreDep [library]
mt1 [lemma, in mt1]
mt2 [lemma, in mt2]
mt3 [lemma, in mt3]
mt3' [lemma, in mt3']
mt4 [lemma, in mt4]
mt4' [lemma, in mt4']
Mult [constructor, in Mult]
myNatIndex [definition, in myNatIndex]
myNatIndex_ok [lemma, in myNatIndex_ok]
myTypes [definition, in myTypes]
myValues [definition, in myValues]
my_tauto [definition, in my_tauto]
my_tauto [section, in my_tauto]
my_tauto.atomics [variable, in atomics]
m1 [lemma, in m1]
m2 [lemma, in m2]


N

napp [definition, in napp]
Nat [constructor, in Nat]
Nat [constructor, in Nat]
Nat [constructor, in Nat]
Nat [constructor, in Nat]
Nat [constructor, in Nat]
Nat [constructor, in Nat]
nat [inductive, in nat]
NatFunc [constructor, in NatFunc]
nat_tree_ind'.P [variable, in P]
nat_ind'.P [variable, in P]
nat_tree_ind' [definition, in nat_tree_ind']
nat_tree_ind' [section, in nat_tree_ind']
nat_btree [inductive, in nat_btree]
nat_den [definition, in nat_den]
nat_tree_ind'.NNode'_case [variable, in NNode'_case]
nat_ind'.S_case [variable, in S_case]
nat_ind' [definition, in nat_ind']
nat_ind' [section, in nat_ind']
nat_tree [inductive, in nat_tree]
nat_dt [definition, in nat_dt]
nat_fix [definition, in nat_fix]
nat_list [inductive, in nat_list]
nat_ind'.O_case [variable, in O_case]
nat_rect' [definition, in nat_rect']
nat_eq_dec [lemma, in nat_eq_dec]
NCons [constructor, in NCons]
NConst [constructor, in NConst]
NConst [constructor, in NConst]
needs_trans [definition, in needs_trans]
negb [definition, in negb]
negb_inverse [lemma, in negb_inverse]
negb_ineq [lemma, in negb_ineq]
negb' [definition, in negb']
Next [constructor, in Next]
Nil [constructor, in Nil]
Nil [constructor, in Nil]
Nil [constructor, in Nil]
Nil [constructor, in Nil]
Nil [constructor, in Nil]
NLeaf [constructor, in NLeaf]
nlength [definition, in nlength]
nlength_napp [lemma, in nlength_napp]
NNil [constructor, in NNil]
NNode [constructor, in NNode]
NNode' [constructor, in NNode']
noBadChains [lemma, in noBadChains]
noBadChains' [lemma, in noBadChains']
Node [constructor, in Node]
Node [constructor, in Node]
Node [constructor, in Node]
nonrecursive [projection, in nonrecursive]
noot [definition, in noot]
not_classic [axiom, in not_classic]
nsize [definition, in nsize]
nsize_nsplice [lemma, in nsize_nsplice]
nsplice [definition, in nsplice]
nth_error_nil [lemma, in nth_error_nil]
ntsize [definition, in ntsize]
ntsize_ntsplice [lemma, in ntsize_ntsplice]
ntsplice [definition, in ntsplice]
num [axiom, in num]
nvm [definition, in nvm]
n_plus_O [lemma, in n_plus_O]
n_plus_O' [lemma, in n_plus_O']


O

O [constructor, in O]
oapp [definition, in oapp]
obvious [lemma, in obvious]
obvious' [lemma, in obvious']
OCons [constructor, in OCons]
odd_list_mut [definition, in odd_list_mut]
odd_list [inductive, in odd_list]
odd_list_mut' [definition, in odd_list_mut']
ok [section, in ok]
ok.dd [variable, in dd]
ok.dt [variable, in dt]
ok.fx [variable, in fx]
ok.T [variable, in T]
olength [definition, in olength]
ones [definition, in ones]
ones_eq'' [lemma, in ones_eq'']
ones_eq [lemma, in ones_eq]
ones_eq [lemma, in ones_eq]
ones_eq [lemma, in ones_eq]
ones_eq' [lemma, in ones_eq']
ones_eq''' [lemma, in ones_eq''']
ones' [definition, in ones']
Op [constructor, in Op]
optCmd [definition, in optCmd]
optCmd_correct [lemma, in optCmd_correct]
optCmd_correct1 [lemma, in optCmd_correct1]
optCmd_correct2 [lemma, in optCmd_correct2]
optExp [definition, in optExp]
optExp_correct [lemma, in optExp_correct]
Or [constructor, in Or]
Or [constructor, in Or]
Or [constructor, in Or]
or [inductive, in or]
or_comm' [lemma, in or_comm']
or_introl [constructor, in or_introl]
or_intror [constructor, in or_intror]
or_comm [lemma, in or_comm]
or_assoc [lemma, in or_assoc]
Or' [constructor, in Or']
Or' [constructor, in Or']
out_of_luck [lemma, in out_of_luck]
O_plus_n [lemma, in O_plus_n]


P

paartial [definition, in paartial]
Pair [constructor, in Pair]
Pair [constructor, in Pair]
pair [constructor, in pair]
pairOut [definition, in pairOut]
pairOutType [definition, in pairOutType]
PairP [constructor, in PairP]
pair_cong [lemma, in pair_cong]
pair' [constructor, in pair']
PAnd [constructor, in PAnd]
partialOut [definition, in partialOut]
pformula [inductive, in pformula]
pformulaDenote [definition, in pformulaDenote]
PI [constructor, in PI]
pick_conc1 [lemma, in pick_conc1]
pick_conc2 [lemma, in pick_conc2]
pick_prem1 [lemma, in pick_prem1]
pick_prem2 [lemma, in pick_prem2]
PInject [constructor, in PInject]
Plus [constructor, in Plus]
Plus [constructor, in Plus]
Plus [constructor, in Plus]
Plus [constructor, in Plus]
Plus [constructor, in Plus]
Plus [constructor, in Plus]
Plus [constructor, in Plus]
Plus [constructor, in Plus]
Plus [constructor, in Plus]
plus [definition, in plus]
PlusO [constructor, in PlusO]
plusO [lemma, in plusO]
plusO' [lemma, in plusO']
plusR [inductive, in plusR]
plusR_plus [lemma, in plusR_plus]
PlusS [constructor, in PlusS]
plusS [lemma, in plusS]
plus_assoc [lemma, in plus_assoc]
plus_ge [lemma, in plus_ge]
plus_n_Sm' [lemma, in plus_n_Sm']
plus_recursive [definition, in plus_recursive]
plus_rec [definition, in plus_rec]
plus_plusR [lemma, in plus_plusR]
plus_0 [lemma, in plus_0]
plus_S [lemma, in plus_S]
plus_equivalent [lemma, in plus_equivalent]
plus1 [lemma, in plus1]
positive [axiom, in positive]
pred [definition, in pred]
Predicates [library]
predicate_extensionality [lemma, in predicate_extensionality]
pred_strong1_irrel [lemma, in pred_strong1_irrel]
pred_strong1_irrel' [lemma, in pred_strong1_irrel']
pred_strong1 [definition, in pred_strong1]
pred_strong1 [definition, in pred_strong1]
pred_strong2 [definition, in pred_strong2]
pred_strong3 [definition, in pred_strong3]
pred_strong4 [definition, in pred_strong4]
pred_strong5 [definition, in pred_strong5]
pred_strong6 [definition, in pred_strong6]
pred_strong7 [definition, in pred_strong7]
pred_strong8 [definition, in pred_strong8]
pred_strong1' [definition, in pred_strong1']
pred_strong4' [definition, in pred_strong4']
pred_strong [definition, in pred_strong]
pred' [definition, in pred']
pred' [definition, in pred']
present [definition, in present]
present [section, in present]
present_ins [lemma, in present_ins]
present_insert_Black [lemma, in present_insert_Black]
present_balance1 [lemma, in present_balance1]
present_balance2 [lemma, in present_balance2]
present_insResult [definition, in present_insResult]
present_insert_Red [lemma, in present_insert_Red]
present.x [variable, in x]
print [definition, in print]
printName [projection, in printName]
printNonrec [projection, in printNonrec]
print_datatype [definition, in print_datatype]
print_constructor [record, in print_constructor]
print_nat [definition, in print_nat]
Prod [constructor, in Prod]
prod [inductive, in prod]
prod [inductive, in prod]
prod' [inductive, in prod']
prod' [definition, in prod']
prog [definition, in prog]
progDenote [definition, in progDenote]
ProgLang [library]
projE [definition, in projE]
projS [definition, in projS]
proj1 [lemma, in proj1]
proj1_again' [lemma, in proj1_again']
proj1_again [lemma, in proj1_again]
proj1_again'' [lemma, in proj1_again'']
proof [inductive, in proof]
prop [inductive, in prop]
propify [definition, in propify]
propify_holds [lemma, in propify_holds]
propify_holds' [lemma, in propify_holds']
Propositional [section, in Propositional]
propositional [lemma, in propositional]
propositional [section, in propositional]
propositional.P [variable, in P]
Propositional.P [variable, in P]
propositional.Q [variable, in Q]
Propositional.Q [variable, in Q]
propositional.R [variable, in R]
Propositional.R [variable, in R]
prop' [inductive, in prop']


R

rbtree [inductive, in rbtree]
reassoc [definition, in reassoc]
reassoc_correct [lemma, in reassoc_correct]
reassoc_correct [lemma, in reassoc_correct]
reassoc_correct [lemma, in reassoc_correct]
recursive [projection, in recursive]
Red [constructor, in Red]
RedNode [constructor, in RedNode]
RedNode' [constructor, in RedNode']
reduce_me [lemma, in reduce_me]
red_herring [definition, in red_herring]
red_herring [definition, in red_herring]
red_herring [definition, in red_herring]
red_herring [definition, in red_herring]
red_herring [definition, in red_herring]
red_herring [definition, in red_herring]
red_herring [definition, in red_herring]
Reflection [library]
regexp [inductive, in regexp]
Ret [constructor, in Ret]
Return [definition, in Return]
Return [section, in Return]
Return.A [variable, in A]
Return.v [variable, in v]
rewr [lemma, in rewr]
rifoldr [definition, in rifoldr]
rifoldr [section, in rifoldr]
rifoldr.A [variable, in A]
rifoldr.B [variable, in B]
rifoldr.f [variable, in f]
rifoldr.i [variable, in i]
right_identity [lemma, in right_identity]
rpresent [definition, in rpresent]
rtree [inductive, in rtree]
run [definition, in run]
runTo [definition, in runTo]
run_Fix [lemma, in run_Fix]
run_Bottom [lemma, in run_Bottom]
run_Bind [lemma, in run_Bind]
run_Return [lemma, in run_Return]


S

S [constructor, in S]
Seq [constructor, in Seq]
set [definition, in set]
seven_minus_four [definition, in seven_minus_four]
seven_minus_three'' [definition, in seven_minus_three'']
seven_minus_three [definition, in seven_minus_three]
seven_minus_three' [definition, in seven_minus_three']
seven_minus_four' [definition, in seven_minus_four']
seven_minus_four_zero [definition, in seven_minus_four_zero]
seven_minus_four_zero [definition, in seven_minus_four_zero]
seven_minus_three_again [definition, in seven_minus_three_again]
size [definition, in size]
size_positive [lemma, in size_positive]
skipCopies [definition, in skipCopies]
slow [lemma, in slow]
slow [section, in slow]
slow [section, in slow]
slow' [lemma, in slow']
slow.A [variable, in A]
slow.f [variable, in f]
slow.H1 [variable, in H1]
slow.H2 [variable, in H2]
slow.H3 [variable, in H3]
slow.P [variable, in P]
slow.Q [variable, in Q]
slow.R [variable, in R]
slow.S [variable, in S]
Snd [constructor, in Snd]
somePairs [definition, in somePairs]
someTypes [definition, in someTypes]
someValues [definition, in someValues]
Some_inj [lemma, in Some_inj]
split [definition, in split]
split [section, in split]
split [definition, in split]
split_wf1 [lemma, in split_wf1]
split_wf2 [lemma, in split_wf2]
split_wf [lemma, in split_wf]
split' [definition, in split']
split.P1 [variable, in P1]
split.P1_dec [variable, in P1_dec]
split.P2 [variable, in P2]
split.P2_dec [variable, in P2_dec]
split.s [variable, in s]
stack [definition, in stack]
StackMachine [library]
Star [constructor, in Star]
star [inductive, in star]
star [section, in star]
star_app [lemma, in star_app]
star_substring_inv [lemma, in star_substring_inv]
star_empty [lemma, in star_empty]
star_singleton [lemma, in star_singleton]
star_length_flip [lemma, in star_length_flip]
star_length_contra [lemma, in star_length_contra]
star_inv [lemma, in star_inv]
star.P [variable, in P]
stream [inductive, in stream]
stream [section, in stream]
stream_eq_onequant.Cons_case_hd [variable, in Cons_case_hd]
stream_eq_loop.Cons_case_hd [variable, in Cons_case_hd]
stream_eq_coind.Cons_case_hd [variable, in Cons_case_hd]
stream_eq_onequant.A [variable, in A]
stream_eq_loop.A [variable, in A]
stream_eq_coind.A [variable, in A]
stream_eq.A [variable, in A]
stream_eq_onequant.B [variable, in B]
stream_eq_coind.R [variable, in R]
stream_eq_onequant.f [variable, in f]
stream_eq_onequant.g [variable, in g]
stream_eq_onequant.Cons_case_tl [variable, in Cons_case_tl]
stream_eq_coind.Cons_case_tl [variable, in Cons_case_tl]
Stream_eq [constructor, in Stream_eq]
stream_eq_loop [lemma, in stream_eq_loop]
stream_eq_loop [section, in stream_eq_loop]
stream_eq_loop.s1 [variable, in s1]
stream_eq_loop.s2 [variable, in s2]
stream_eq_coind [lemma, in stream_eq_coind]
stream_eq_coind [section, in stream_eq_coind]
stream_eq_onequant [lemma, in stream_eq_onequant]
stream_eq_onequant [section, in stream_eq_onequant]
stream_eq [inductive, in stream_eq]
stream_eq [section, in stream_eq]
stream_eq_loop.loop1 [variable, in loop1]
stream_eq_loop.loop2 [variable, in loop2]
stream.A [variable, in A]
Streicher_K' [definition, in Streicher_K']
Subset [library]
substring_suffix_emp [lemma, in substring_suffix_emp]
substring_app_fst [lemma, in substring_app_fst]
substring_suffix [lemma, in substring_suffix]
substring_self [lemma, in substring_self]
substring_all [lemma, in substring_all]
substring_split' [lemma, in substring_split']
substring_stack' [lemma, in substring_stack']
substring_empty [lemma, in substring_empty]
substring_none [lemma, in substring_none]
substring_suffix_emp' [lemma, in substring_suffix_emp']
substring_le [lemma, in substring_le]
substring_stack [lemma, in substring_stack]
substring_split [lemma, in substring_split]
substring_app_snd [lemma, in substring_app_snd]
sum [definition, in sum]
sum [definition, in sum]
sum [definition, in sum]
sum [inductive, in sum]
sum [definition, in sum]
sumboool [definition, in sumboool]
sum_inc' [lemma, in sum_inc']
sum_inc [lemma, in sum_inc]
sum_inc [lemma, in sum_inc]
swapper [definition, in swapper]
swapper_preserves_truth [lemma, in swapper_preserves_truth]
symmetry [lemma, in symmetry]
syms [definition, in syms]
sym_sig [definition, in sym_sig]
sym_ex [definition, in sym_ex]
synthesize1 [definition, in synthesize1]
synthesize2 [definition, in synthesize2]
synthesize3 [definition, in synthesize3]
S_inj [lemma, in S_inj]
S_inj' [lemma, in S_inj']


T

tassociativity [lemma, in tassociativity]
taut [inductive, in taut]
TautAnd [constructor, in TautAnd]
tautDenote [definition, in tautDenote]
TautImp [constructor, in TautImp]
TautOr [constructor, in TautOr]
TautTrue [constructor, in TautTrue]
tautTrue [lemma, in tautTrue]
TBConst [constructor, in TBConst]
TBind [definition, in TBind]
TBind_Answer [lemma, in TBind_Answer]
TBinop [constructor, in TBinop]
tbinop [inductive, in tbinop]
tbinopDenote [definition, in tbinopDenote]
TBool [constructor, in TBool]
tcompile [definition, in tcompile]
tcompile_correct' [lemma, in tcompile_correct']
tcompile_correct' [lemma, in tcompile_correct']
tcompile_correct [lemma, in tcompile_correct]
tcompile_correct [lemma, in tcompile_correct]
tconcat [definition, in tconcat]
tconcat_correct [lemma, in tconcat_correct]
TCons [constructor, in TCons]
TEq [constructor, in TEq]
term [inductive, in term]
term [inductive, in term]
termDenote [definition, in termDenote]
testCurriedAdd [definition, in testCurriedAdd]
test_inster.A [variable, in A]
test_inster.P [variable, in P]
test_inster.Q [variable, in Q]
test_inster.f [variable, in f]
test_inster.g [variable, in g]
test_map [lemma, in test_map]
test_inster2 [lemma, in test_inster2]
test_mergeSort' [lemma, in test_mergeSort']
test_inster [lemma, in test_inster]
test_inster [section, in test_inster]
test_looper [lemma, in test_looper]
test_inster.H1 [variable, in H1]
test_inster.H3 [variable, in H3]
test_inster.H4 [variable, in H4]
test_mergeSort'' [lemma, in test_mergeSort'']
texp [inductive, in texp]
texpDenote [definition, in texpDenote]
tg [definition, in tg]
the_sky_is_falling [lemma, in the_sky_is_falling]
Think [constructor, in Think]
thunk [inductive, in thunk]
thunk_eq_coind.A [variable, in A]
thunk_eq_coind.H [variable, in H]
thunk_eq_coind.P [variable, in P]
thunk_eq_frob [lemma, in thunk_eq_frob]
thunk_eq [inductive, in thunk_eq]
thunk_eq_refl [lemma, in thunk_eq_refl]
thunk_eq_coind [lemma, in thunk_eq_coind]
thunk_eq_coind [section, in thunk_eq_coind]
TiBConst [constructor, in TiBConst]
TiBinop [constructor, in TiBinop]
times [definition, in times]
times [definition, in times]
times [definition, in times]
times [definition, in times]
Times [constructor, in Times]
times_1 [lemma, in times_1]
TiNConst [constructor, in TiNConst]
tinstr [inductive, in tinstr]
tinstrDenote [definition, in tinstrDenote]
tl [definition, in tl]
tleft_identity [lemma, in tleft_identity]
TLt [constructor, in TLt]
TNat [constructor, in TNat]
TNConst [constructor, in TNConst]
TNil [constructor, in TNil]
toProp [definition, in toProp]
TPlus [constructor, in TPlus]
tprog [inductive, in tprog]
tprogDenote [definition, in tprogDenote]
tree [inductive, in tree]
tree [section, in tree]
tree [inductive, in tree]
tree [section, in tree]
tree [inductive, in tree]
tree [section, in tree]
tree_den [definition, in tree_den]
tree_fix [definition, in tree_fix]
tree_dt [definition, in tree_dt]
tree.A [variable, in A]
tree.A [variable, in A]
tree.A [variable, in A]
tright_identity [lemma, in tright_identity]
Tru [constructor, in Tru]
true [constructor, in true]
true [constructor, in true]
trues_falses [definition, in trues_falses]
true_galore [lemma, in true_galore]
true_neq_false [lemma, in true_neq_false]
True_conc [lemma, in True_conc]
true_galore' [lemma, in true_galore']
Truth [constructor, in Truth]
Truth [constructor, in Truth]
Truth' [constructor, in Truth']
Tru' [constructor, in Tru']
tstack [definition, in tstack]
tt [constructor, in tt]
tt [constructor, in tt]
TTimes [constructor, in TTimes]
twoEls [inductive, in twoEls]
twoEls [section, in twoEls]
TwoEls [constructor, in TwoEls]
twoEls_nil [lemma, in twoEls_nil]
twoEls_two [lemma, in twoEls_two]
twoEls.A [variable, in A]
two_gt0 [lemma, in two_gt0]
two_funs [lemma, in two_funs]
type [inductive, in type]
type [inductive, in type]
type [inductive, in type]
type [inductive, in type]
type [inductive, in type]
type [inductive, in type]
typeCheck [definition, in typeCheck]
typeCheck' [definition, in typeCheck']
typeDenote [definition, in typeDenote]
typeDenote [definition, in typeDenote]
typeDenote [definition, in typeDenote]
typeDenote [definition, in typeDenote]
typeDenote [definition, in typeDenote]
types' [definition, in types']
type' [inductive, in type']
type'Denote [definition, in type'Denote]
t1 [lemma, in t1]
t1 [lemma, in t1]
t1 [lemma, in t1]
t1' [lemma, in t1']
t2 [lemma, in t2]
t2 [lemma, in t2]
t2' [lemma, in t2']
t3 [lemma, in t3]
t3 [lemma, in t3]
t3 [lemma, in t3]
t4 [lemma, in t4]
t4 [lemma, in t4]
t5 [lemma, in t5]
t5' [lemma, in t5']
t6 [lemma, in t6]
t6 [section, in t6]
t6.A [variable, in A]
t6.B [variable, in B]
t6.f [variable, in f]
t6.g [variable, in g]
t6.H1 [variable, in H1]
t6.H2 [variable, in H2]
t6.P [variable, in P]
t7 [lemma, in t7]
t7 [section, in t7]
t7 [lemma, in t7]
t7 [section, in t7]
t7.A [variable, in A]
t7.A [variable, in A]
t7.B [variable, in B]
t7.B [variable, in B]
t7.f [variable, in f]
t7.f [variable, in f]
t7.g [variable, in g]
t7.g [variable, in g]
t7.H1 [variable, in H1]
t7.H1 [variable, in H1]
t7.H2 [variable, in H2]
t7.H2 [variable, in H2]
t7.P [variable, in P]
t7.P [variable, in P]
t7.Q [variable, in Q]
t7.Q [variable, in Q]
t8 [lemma, in t8]
t9 [lemma, in t9]


U

ugh [definition, in ugh]
uhoh [lemma, in uhoh]
uhoh [definition, in uhoh]
uhoh_again [lemma, in uhoh_again]
UIP [lemma, in UIP]
UIP_refl [lemma, in UIP_refl]
UIP_refl'' [lemma, in UIP_refl'']
UIP_refl' [definition, in UIP_refl']
unique_ident [lemma, in unique_ident]
Unit [constructor, in Unit]
unit [inductive, in unit]
unit [inductive, in unit]
unit_fix [definition, in unit_fix]
unit_dt [definition, in unit_dt]
unit_singleton [lemma, in unit_singleton]
unit_den [definition, in unit_den]
Universes [library]
unject [definition, in unject]
Unknown [constructor, in Unknown]
update [definition, in update]


V

Var [constructor, in Var]
Var [constructor, in Var]
Var [constructor, in Var]
Var [constructor, in Var]
var [definition, in var]
VarEq [constructor, in VarEq]
vars [definition, in vars]
vstack [definition, in vstack]


W

While [constructor, in While]
withTypes [section, in withTypes]
withTypes' [section, in withTypes']
withTypes'.natIndex [variable, in natIndex]
withTypes'.types [variable, in types]
withTypes'.values [variable, in values]
withTypes.natIndex [variable, in natIndex]
withTypes.natIndex_ok [variable, in natIndex_ok]
withTypes.types [variable, in types]
withTypes.values [variable, in values]


Z

zeroes [definition, in zeroes]
zero_minus_one [definition, in zero_minus_one]
zero_times [lemma, in zero_times]
zgtz [lemma, in zgtz]
zgtz [lemma, in zgtz]


other

_ == _ [notation, in ::x_'=='_x]
_ ;;; _ [notation, in ::x_';;;'_x]
_ || _ [notation, in ::x_'||'_x]
_ <-- _ ; _ [notation, in ::x_'<--'_x_';'_x]
_ === _ [notation, in ::x_'==='_x]
_ <- _ ; _ [notation, in ::x_'<-'_x_';'_x]
_ <- _ ; _ [notation, in ::x_'<-'_x_';'_x]
_ <- _ ; _ [notation, in ::x_'<-'_x_';'_x]
_ <- _ ; _ [notation, in ::x_'<-'_x_';'_x]
_ --> _ [notation, in ::x_'-->'_x]
_ --> _ [notation, in ::x_'-->'_x]
_ ;; _ [notation, in ::x_';;'_x]
No [notation, in ::'No']
Reduce _ [notation, in ::'Reduce'_x]
Yes [notation, in ::'Yes']
!! [notation, in ::'!!']
! [notation, in ::'!']
?? [notation, in ::'??']
[ _ ] [notation, in ::'['_x_']']
[ _ , _ ~> _ ] [notation, in ::'['_x_','_x_'~>'_x_']']
[| _ |] [notation, in ::'[|'_x_'|]']
[|| _ ||] [notation, in ::'[||'_x_'||]']
^ [notation, in ::'^']
{< _ >} [notation, in ::'{<'_x_'>}']
{{ _ | _ }} [notation, in ::'{{'_x_'|'_x_'}}']


Projection Index

H

HigherOrder.First [in First]
HigherOrder.Second [in Second]
HigherOrder.Ty [in Ty]


N

nonrecursive [in nonrecursive]


P

printName [in printName]
printNonrec [in printNonrec]


R

recursive [in recursive]


Record Index

C

constructor [in constructor]


H

HigherOrder.varEntry [in varEntry]


P

print_constructor [in print_constructor]


Lemma Index

A

allTrue_add [in allTrue_add]
allTrue_In [in allTrue_In]
and_assoc [in and_assoc]
and_True_prem [in and_True_prem]
and_True_conc [in and_True_conc]
and_comm [in and_comm]
append_emp [in append_emp]
app_cong [in app_cong]
app_empty_end [in app_empty_end]
arith_neq' [in arith_neq']
arith_comm [in arith_comm]
arith_comm' [in arith_comm']
arith_neq [in arith_neq]
associativity [in associativity]


B

balanced [in balanced]
bool_neq [in bool_neq]
bool_neq [in bool_neq]


C

cassociativity [in cassociativity]
cassociativity1 [in cassociativity1]
cassociativity2 [in cassociativity2]
cfoldCond_correct [in cfoldCond_correct]
cfold_correct [in cfold_correct]
cfold_correct [in cfold_correct]
cfold_correct [in cfold_correct]
cfold_correct [in cfold_correct]
cfold_correct [in cfold_correct]
cleft_identity [in cleft_identity]
combine [in combine]
comm_conc [in comm_conc]
comm_prem [in comm_prem]
compile_correct [in compile_correct]
compile_correct [in compile_correct]
compile_correct' [in compile_correct']
compile_correct' [in compile_correct']
cond_ext [in cond_ext]
confounder [in confounder]
contra [in contra]
cright_identity [in cright_identity]


D

depth_max' [in depth_max']
depth_max [in depth_max]
depth_max [in depth_max]
depth_min [in depth_min]


E

elength_eapp [in elength_eapp]
elength_eapp [in elength_eapp]
evalCmd_coind [in evalCmd_coind]
EvalConst' [in EvalConst']
EvalPlus' [in EvalPlus']
EvalVar' [in EvalVar']
eval_fact [in eval_fact]
eval_frob [in eval_frob]
eval_times [in eval_times]
eval_times [in eval_times]
eval_times [in eval_times]
eval_times [in eval_times]
eval_times [in eval_times]
eval_times [in eval_times]
eval_times [in eval_times]
eval_times [in eval_times]
even_1_contra [in even_1_contra]
even_4' [in even_4']
even_plus [in even_plus]
even_256' [in even_256']
even_255 [in even_255]
even_256 [in even_256]
even_contra' [in even_contra']
even_3_contra [in even_3_contra]
even_0 [in even_0]
even_4 [in even_4]
even_contra [in even_contra]
even_contra [in even_contra]
even_contra'' [in even_contra'']
exec_frob [in exec_frob]
exist1 [in exist1]
exist2 [in exist2]
ex_irrelevant [in ex_irrelevant]
ex_prem [in ex_prem]
ex_conc [in ex_conc]
ex_symmetry [in ex_symmetry]


F

fact_def [in fact_def]
fact_eq [in fact_eq]
fact_eq' [in fact_eq']
fact_eq'' [in fact_eq'']
falseFree_holds [in falseFree_holds]
False_imp [in False_imp]
False_prem [in False_prem]
fhapp_assoc'' [in fhapp_assoc'']
fhapp_assoc' [in fhapp_assoc']
fhapp_assoc [in fhapp_assoc]
fhget_fhmap [in fhget_fhmap]
fin_cases [in fin_cases]
fin_cases_again [in fin_cases_again]
fin_cases_again' [in fin_cases_again']
FirstOrder.cfoldSound [in cfoldSound]
FirstOrder.identSound [in identSound]
FirstOrder.liftSound [in liftSound]
FirstOrder.liftVarSound [in liftVarSound]
FirstOrder.lift'Sound [in lift'Sound]
FirstOrder.unletSound [in unletSound]
FirstOrder.unletSound' [in unletSound']
Fix'_ok [in Fix'_ok]
flatten_correct' [in flatten_correct']
flatten_correct [in flatten_correct]
fo [in fo]
foldr_plus [in foldr_plus]
Forall_weaken [in Forall_weaken]
forall_exists_commute [in forall_exists_commute]
Forall_In' [in Forall_In']
forall_eq [in forall_eq]
Forall_In [in Forall_In]
forall_and [in forall_and]
fo' [in fo']
frob_eq [in frob_eq]
frob_eq [in frob_eq]
f_f_f_g [in f_f_f_g]
f_f_f [in f_f_f]
f_f_f' [in f_f_f']
f_f_f' [in f_f_f']
f_f_f' [in f_f_f']


G

getNat_is_reasonable [in getNat_is_reasonable]
getNat_is_reasonable [in getNat_is_reasonable]
get_imap [in get_imap]
ge_refl [in ge_refl]
GroupProofs.ident' [in ident']
GroupProofs.inverse' [in inverse']
GroupProofs.unique_ident [in unique_ident]


H

hasType_det [in hasType_det]
HigherOrder.CfoldSound [in CfoldSound]
HigherOrder.cfoldSound [in cfoldSound]
HigherOrder.IdentSound [in IdentSound]
HigherOrder.identSound [in identSound]
HigherOrder.three_the_hard_way_Wf [in three_the_hard_way_Wf]
HigherOrder.UnletSound [in UnletSound]
HigherOrder.unletSound [in unletSound]
HigherOrder.unletWf [in unletWf]
HigherOrder.UnletWf [in UnletWf]
HigherOrder.wf_monotone [in wf_monotone]
hmap_hmap [in hmap_hmap]
hmm [in hmm]
hmm' [in hmm']
hmm2 [in hmm2]


I

illustrative_but_silly_detour [in illustrative_but_silly_detour]
illustrative_but_silly_detour [in illustrative_but_silly_detour]
imp_True [in imp_True]
inject_inverse [in inject_inverse]
Int.assoc [in assoc]
Int.ident [in ident]
Int.inverse [in inverse]
in_star [in in_star]
isZero_contra' [in isZero_contra']
isZero_plus [in isZero_plus]
isZero_zero [in isZero_zero]
isZero_contra [in isZero_contra]


J

JMeq_refl' [in JMeq_refl']
JMeq_eq' [in JMeq_eq']


L

left_identity [in left_identity]
lemma1 [in lemma1]
lemma2 [in lemma2]
lemma3 [in lemma3]
lemma3 [in lemma3]
lemma4 [in lemma4]
lengthOrder_wf [in lengthOrder_wf]
lengthOrder_wf' [in lengthOrder_wf']
length_emp [in length_emp]
length_app [in length_app]
length_app [in length_app]
length_app1 [in length_app1]
length_O [in length_O]
length_S [in length_S]
leq_Some [in leq_Some]
leq_None [in leq_None]
linear [in linear]


M

map_id [in map_id]
Match [in Match]
max_spec_le [in max_spec_le]
max_1 [in max_1]
max_2 [in max_2]
mergeSort_eq [in mergeSort_eq]
minus_minus [in minus_minus]
monoid_reflect [in monoid_reflect]
mt1 [in mt1]
mt2 [in mt2]
mt3 [in mt3]
mt3' [in mt3']
mt4 [in mt4]
mt4' [in mt4']
myNatIndex_ok [in myNatIndex_ok]
m1 [in m1]
m2 [in m2]


N

nat_eq_dec [in nat_eq_dec]
negb_inverse [in negb_inverse]
negb_ineq [in negb_ineq]
nlength_napp [in nlength_napp]
noBadChains [in noBadChains]
noBadChains' [in noBadChains']
nsize_nsplice [in nsize_nsplice]
nth_error_nil [in nth_error_nil]
ntsize_ntsplice [in ntsize_ntsplice]
n_plus_O [in n_plus_O]
n_plus_O' [in n_plus_O']


O

obvious [in obvious]
obvious' [in obvious']
ones_eq'' [in ones_eq'']
ones_eq [in ones_eq]
ones_eq [in ones_eq]
ones_eq [in ones_eq]
ones_eq' [in ones_eq']
ones_eq''' [in ones_eq''']
optCmd_correct [in optCmd_correct]
optCmd_correct1 [in optCmd_correct1]
optCmd_correct2 [in optCmd_correct2]
optExp_correct [in optExp_correct]
or_comm' [in or_comm']
or_comm [in or_comm]
or_assoc [in or_assoc]
out_of_luck [in out_of_luck]
O_plus_n [in O_plus_n]


P

pair_cong [in pair_cong]
pick_conc1 [in pick_conc1]
pick_conc2 [in pick_conc2]
pick_prem1 [in pick_prem1]
pick_prem2 [in pick_prem2]
plusO [in plusO]
plusO' [in plusO']
plusR_plus [in plusR_plus]
plusS [in plusS]
plus_assoc [in plus_assoc]
plus_ge [in plus_ge]
plus_n_Sm' [in plus_n_Sm']
plus_plusR [in plus_plusR]
plus_0 [in plus_0]
plus_S [in plus_S]
plus_equivalent [in plus_equivalent]
plus1 [in plus1]
predicate_extensionality [in predicate_extensionality]
pred_strong1_irrel [in pred_strong1_irrel]
pred_strong1_irrel' [in pred_strong1_irrel']
present_ins [in present_ins]
present_insert_Black [in present_insert_Black]
present_balance1 [in present_balance1]
present_balance2 [in present_balance2]
present_insert_Red [in present_insert_Red]
proj1 [in proj1]
proj1_again' [in proj1_again']
proj1_again [in proj1_again]
proj1_again'' [in proj1_again'']
propify_holds [in propify_holds]
propify_holds' [in propify_holds']
propositional [in propositional]


R

reassoc_correct [in reassoc_correct]
reassoc_correct [in reassoc_correct]
reassoc_correct [in reassoc_correct]
reduce_me [in reduce_me]
rewr [in rewr]
right_identity [in right_identity]
run_Fix [in run_Fix]
run_Bottom [in run_Bottom]
run_Bind [in run_Bind]
run_Return [in run_Return]


S

size_positive [in size_positive]
slow [in slow]
slow' [in slow']
Some_inj [in Some_inj]
split_wf1 [in split_wf1]
split_wf2 [in split_wf2]
split_wf [in split_wf]
star_app [in star_app]
star_substring_inv [in star_substring_inv]
star_empty [in star_empty]
star_singleton [in star_singleton]
star_length_flip [in star_length_flip]
star_length_contra [in star_length_contra]
star_inv [in star_inv]
stream_eq_loop [in stream_eq_loop]
stream_eq_coind [in stream_eq_coind]
stream_eq_onequant [in stream_eq_onequant]
substring_suffix_emp [in substring_suffix_emp]
substring_app_fst [in substring_app_fst]
substring_suffix [in substring_suffix]
substring_self [in substring_self]
substring_all [in substring_all]
substring_split' [in substring_split']
substring_stack' [in substring_stack']
substring_empty [in substring_empty]
substring_none [in substring_none]
substring_suffix_emp' [in substring_suffix_emp']
substring_le [in substring_le]
substring_stack [in substring_stack]
substring_split [in substring_split]
substring_app_snd [in substring_app_snd]
sum_inc' [in sum_inc']
sum_inc [in sum_inc]
sum_inc [in sum_inc]
swapper_preserves_truth [in swapper_preserves_truth]
symmetry [in symmetry]
S_inj [in S_inj]
S_inj' [in S_inj']


T

tassociativity [in tassociativity]
tautTrue [in tautTrue]
TBind_Answer [in TBind_Answer]
tcompile_correct' [in tcompile_correct']
tcompile_correct' [in tcompile_correct']
tcompile_correct [in tcompile_correct]
tcompile_correct [in tcompile_correct]
tconcat_correct [in tconcat_correct]
test_map [in test_map]
test_inster2 [in test_inster2]
test_mergeSort' [in test_mergeSort']
test_inster [in test_inster]
test_looper [in test_looper]
test_mergeSort'' [in test_mergeSort'']
the_sky_is_falling [in the_sky_is_falling]
thunk_eq_frob [in thunk_eq_frob]
thunk_eq_refl [in thunk_eq_refl]
thunk_eq_coind [in thunk_eq_coind]
times_1 [in times_1]
tleft_identity [in tleft_identity]
tright_identity [in tright_identity]
true_galore [in true_galore]
true_neq_false [in true_neq_false]
True_conc [in True_conc]
true_galore' [in true_galore']
twoEls_nil [in twoEls_nil]
twoEls_two [in twoEls_two]
two_gt0 [in two_gt0]
two_funs [in two_funs]
t1 [in t1]
t1 [in t1]
t1 [in t1]
t1' [in t1']
t2 [in t2]
t2 [in t2]
t2' [in t2']
t3 [in t3]
t3 [in t3]
t3 [in t3]
t4 [in t4]
t4 [in t4]
t5 [in t5]
t5' [in t5']
t6 [in t6]
t7 [in t7]
t7 [in t7]
t8 [in t8]
t9 [in t9]


U

uhoh [in uhoh]
uhoh_again [in uhoh_again]
UIP [in UIP]
UIP_refl [in UIP_refl]
UIP_refl'' [in UIP_refl'']
unique_ident [in unique_ident]
unit_singleton [in unit_singleton]


Z

zero_times [in zero_times]
zgtz [in zgtz]
zgtz [in zgtz]


Section Index

A

All [in All]
autorewrite [in autorewrite]
autorewrite.garden_path [in garden_path]
autorewrite.garden_path [in garden_path]
autorewrite.garden_path [in garden_path]


B

Bind [in Bind]
Bottom [in Bottom]


C

cfoldCond [in cfoldCond]
computation [in computation]
cond [in cond]


D

dec_star.dec_star'' [in dec_star'']
dec_star [in dec_star]
denote [in denote]
depth [in depth]


E

evalCmd_coind [in evalCmd_coind]
even_list_mut' [in even_list_mut']


F

fhapp [in fhapp]
fhapp' [in fhapp']
fhapp'' [in fhapp'']
fhlist [in fhlist]
fhlist [in fhlist]
fhlist_map [in fhlist_map]
filist [in filist]
firstorder [in firstorder]
firstorder' [in firstorder']
Fix [in Fix]
Forall [in Forall]
forall_and [in forall_and]
formula_ind' [in formula_ind']


H

HigherOrder.var [in var]
HigherOrder.wf [in wf]
hlist [in hlist]
hmap [in hmap]


I

ifoldr [in ifoldr]
ilist [in ilist]
ilist [in ilist]
ilist_map [in ilist_map]
insert [in insert]
insert.present [in present]
interleave [in interleave]
In_dec [in In_dec]


L

lattice [in lattice]
list [in list]


M

map [in map]
map [in map]
map' [in map']
mergeSort [in mergeSort]
monoid [in monoid]
my_tauto [in my_tauto]


N

nat_tree_ind' [in nat_tree_ind']
nat_ind' [in nat_ind']


O

ok [in ok]


P

present [in present]
Propositional [in Propositional]
propositional [in propositional]


R

Return [in Return]
rifoldr [in rifoldr]


S

slow [in slow]
slow [in slow]
split [in split]
star [in star]
stream [in stream]
stream_eq_loop [in stream_eq_loop]
stream_eq_coind [in stream_eq_coind]
stream_eq_onequant [in stream_eq_onequant]
stream_eq [in stream_eq]


T

test_inster [in test_inster]
thunk_eq_coind [in thunk_eq_coind]
tree [in tree]
tree [in tree]
tree [in tree]
twoEls [in twoEls]
t6 [in t6]
t7 [in t7]
t7 [in t7]


W

withTypes [in withTypes]
withTypes' [in withTypes']


Constructor Index

A

Abs [in Abs]
Abs [in Abs]
Abs [in Abs]
And [in And]
And [in And]
And [in And]
And [in And]
And [in And]
And [in And]
And' [in And']
And' [in And']
Answer [in Answer]
App [in App]
App [in App]
Arrow [in Arrow]
Assign [in Assign]
Atomic [in Atomic]
Atomic' [in Atomic']


B

Bar [in Bar]
Base [in Base]
BConst [in BConst]
BConst [in BConst]
Binop [in Binop]
Black [in Black]
BlackNode [in BlackNode]
Bnd [in Bnd]
Bool [in Bool]
Bool [in Bool]
Bool [in Bool]
Bool [in Bool]


C

ChainCons [in ChainCons]
Char [in Char]
Con [in Con]
Concat [in Concat]
Cond [in Cond]
conj [in conj]
Conjunction [in Conjunction]
Cons [in Cons]
Cons [in Cons]
Cons [in Cons]
Cons [in Cons]
Cons [in Cons]
Const [in Const]
Const [in Const]
Const [in Const]
Const [in Const]
Const [in Const]
Const [in Const]
Const [in Const]
Const [in Const]
ConstP [in ConstP]


E

ECons [in ECons]
Empty [in Empty]
ENil [in ENil]
Eq [in Eq]
Eq [in Eq]
Eq [in Eq]
Eq [in Eq]
EqAnswer [in EqAnswer]
EqP [in EqP]
EqThinkL [in EqThinkL]
EqThinkR [in EqThinkR]
eq_refl [in eq_refl]
EvalAnswer [in EvalAnswer]
EvalAssign [in EvalAssign]
EvalConst [in EvalConst]
EvalPlus [in EvalPlus]
EvalSeq [in EvalSeq]
EvalThink [in EvalThink]
EvalVar [in EvalVar]
EvalWhileFalse [in EvalWhileFalse]
EvalWhileTrue [in EvalWhileTrue]
EvenO [in EvenO]
EvenSS [in EvenSS]
Even_SS [in Even_SS]
Even_O [in Even_O]
ExecBnd [in ExecBnd]
ExecRet [in ExecRet]
ex_intro [in ex_intro]


F

Fals [in Fals]
false [in false]
false [in false]
Falsehood [in Falsehood]
Falsehood [in Falsehood]
Falsehood' [in Falsehood']
FFAnd [in FFAnd]
FFNot [in FFNot]
FFTru [in FFTru]
First [in First]
FirstOrder.Abs [in Abs]
FirstOrder.App [in App]
FirstOrder.Const [in Const]
FirstOrder.Let [in Let]
FirstOrder.Plus [in Plus]
FirstOrder.Var [in Var]
Foo [in Foo]
Forall [in Forall]
Forall [in Forall]
Found [in Found]
Fst [in Fst]
Func [in Func]
Func [in Func]


H

HAnd [in HAnd]
HAnd' [in HAnd']
HCons [in HCons]
HFirst [in HFirst]
HigherOrder.Abs [in Abs]
HigherOrder.App [in App]
HigherOrder.Const [in Const]
HigherOrder.Let [in Let]
HigherOrder.Plus [in Plus]
HigherOrder.Var [in Var]
HigherOrder.WfAbs [in WfAbs]
HigherOrder.WfApp [in WfApp]
HigherOrder.WfConst [in WfConst]
HigherOrder.WfLet [in WfLet]
HigherOrder.WfPlus [in WfPlus]
HigherOrder.WfVar [in WfVar]
HNext [in HNext]
HNil [in HNil]
HOr1 [in HOr1]
HOr1' [in HOr1']
HOr2 [in HOr2]
HOr2' [in HOr2']
HtAnd [in HtAnd]
HtBool [in HtBool]
HtNat [in HtNat]
HtPlus [in HtPlus]
HTru [in HTru]
HTru' [in HTru']


I

iBinop [in iBinop]
iConst [in iConst]
Ident [in Ident]
If [in If]
Imp [in Imp]
Imp' [in Imp']
Inject [in Inject]
IsZero [in IsZero]
Iter [in Iter]


L

Leaf [in Leaf]
Leaf [in Leaf]
Leaf [in Leaf]
Leaf [in Leaf]
Lift [in Lift]


M

Mult [in Mult]


N

Nat [in Nat]
Nat [in Nat]
Nat [in Nat]
Nat [in Nat]
Nat [in Nat]
Nat [in Nat]
NatFunc [in NatFunc]
NCons [in NCons]
NConst [in NConst]
NConst [in NConst]
Next [in Next]
Nil [in Nil]
Nil [in Nil]
Nil [in Nil]
Nil [in Nil]
Nil [in Nil]
NLeaf [in NLeaf]
NNil [in NNil]
NNode [in NNode]
NNode' [in NNode']
Node [in Node]
Node [in Node]
Node [in Node]


O

O [in O]
OCons [in OCons]
Op [in Op]
Or [in Or]
Or [in Or]
Or [in Or]
or_introl [in or_introl]
or_intror [in or_intror]
Or' [in Or']
Or' [in Or']


P

Pair [in Pair]
Pair [in Pair]
pair [in pair]
PairP [in PairP]
pair' [in pair']
PAnd [in PAnd]
PI [in PI]
PInject [in PInject]
Plus [in Plus]
Plus [in Plus]
Plus [in Plus]
Plus [in Plus]
Plus [in Plus]
Plus [in Plus]
Plus [in Plus]
Plus [in Plus]
Plus [in Plus]
PlusO [in PlusO]
PlusS [in PlusS]
Prod [in Prod]


R

Red [in Red]
RedNode [in RedNode]
RedNode' [in RedNode']
Ret [in Ret]


S

S [in S]
Seq [in Seq]
Snd [in Snd]
Star [in Star]
Stream_eq [in Stream_eq]


T

TautAnd [in TautAnd]
TautImp [in TautImp]
TautOr [in TautOr]
TautTrue [in TautTrue]
TBConst [in TBConst]
TBinop [in TBinop]
TBool [in TBool]
TCons [in TCons]
TEq [in TEq]
Think [in Think]
TiBConst [in TiBConst]
TiBinop [in TiBinop]
Times [in Times]
TiNConst [in TiNConst]
TLt [in TLt]
TNat [in TNat]
TNConst [in TNConst]
TNil [in TNil]
TPlus [in TPlus]
Tru [in Tru]
true [in true]
true [in true]
Truth [in Truth]
Truth [in Truth]
Truth' [in Truth']
Tru' [in Tru']
tt [in tt]
tt [in tt]
TTimes [in TTimes]
TwoEls [in TwoEls]


U

Unit [in Unit]
Unknown [in Unknown]


V

Var [in Var]
Var [in Var]
Var [in Var]
Var [in Var]
VarEq [in VarEq]


W

While [in While]


Notation Index

H

_ @ _ [in ::x_'@'_x]
_ @+ _ [in ::x_'@+'_x]
_ --> _ [in ::x_'-->'_x]
# [in ::'#']
[ _ ] [in ::'['_x_']']
\ _ : _ , _ [in ::'\'_x_':'_x_','_x]
^ [in ::'^']


M

_ + _ [in ::x_'+'_x]


other

_ == _ [in ::x_'=='_x]
_ ;;; _ [in ::x_';;;'_x]
_ || _ [in ::x_'||'_x]
_ <-- _ ; _ [in ::x_'<--'_x_';'_x]
_ === _ [in ::x_'==='_x]
_ <- _ ; _ [in ::x_'<-'_x_';'_x]
_ <- _ ; _ [in ::x_'<-'_x_';'_x]
_ <- _ ; _ [in ::x_'<-'_x_';'_x]
_ <- _ ; _ [in ::x_'<-'_x_';'_x]
_ --> _ [in ::x_'-->'_x]
_ --> _ [in ::x_'-->'_x]
_ ;; _ [in ::x_';;'_x]
No [in ::'No']
Reduce _ [in ::'Reduce'_x]
Yes [in ::'Yes']
!! [in ::'!!']
! [in ::'!']
?? [in ::'??']
[ _ ] [in ::'['_x_']']
[ _ , _ ~> _ ] [in ::'['_x_','_x_'~>'_x_']']
[| _ |] [in ::'[|'_x_'|]']
[|| _ ||] [in ::'[||'_x_'||]']
^ [in ::'^']
{< _ >} [in ::'{<'_x_'>}']
{{ _ | _ }} [in ::'{{'_x_'|'_x_'}}']


Inductive Index

A

and [in and]


B

bar [in bar]
binop [in binop]
bool [in bool]
bool [in bool]


C

cmd [in cmd]
color [in color]
comp [in comp]


E

Empty_set [in Empty_set]
Empty_set [in Empty_set]
eq [in eq]
eqPlus [in eqPlus]
eval [in eval]
eval [in eval]
evalCmd [in evalCmd]
even [in even]
even_list [in even_list]
evilStream [in evilStream]
ex [in ex]
exec [in exec]
exp [in exp]
exp [in exp]
exp [in exp]
exp [in exp]
exp [in exp]
exp [in exp]
exp [in exp]
exp [in exp]
exp [in exp]
expP [in expP]
exp' [in exp']


F

falseFree [in falseFree]
fin [in fin]
FirstOrder.term [in term]
foo [in foo]
formula [in formula]
formula [in formula]
formula [in formula]
formula' [in formula']


H

hasType [in hasType]
HigherOrder.term [in term]
HigherOrder.wf [in wf]
hlist [in hlist]
holds [in holds]
holds' [in holds']


I

ilist [in ilist]
ilist [in ilist]
infiniteDecreasingChain [in infiniteDecreasingChain]
instr [in instr]
isEven [in isEven]
isZero [in isZero]


L

list [in list]
list [in list]


M

maybe [in maybe]
member [in member]
mexp [in mexp]


N

nat [in nat]
nat_btree [in nat_btree]
nat_tree [in nat_tree]
nat_list [in nat_list]


O

odd_list [in odd_list]
or [in or]


P

pformula [in pformula]
plusR [in plusR]
prod [in prod]
prod [in prod]
prod' [in prod']
proof [in proof]
prop [in prop]
prop' [in prop']


R

rbtree [in rbtree]
regexp [in regexp]
rtree [in rtree]


S

star [in star]
stream [in stream]
stream_eq [in stream_eq]
sum [in sum]


T

taut [in taut]
tbinop [in tbinop]
term [in term]
term [in term]
texp [in texp]
thunk [in thunk]
thunk_eq [in thunk_eq]
tinstr [in tinstr]
tprog [in tprog]
tree [in tree]
tree [in tree]
tree [in tree]
twoEls [in twoEls]
type [in type]
type [in type]
type [in type]
type [in type]
type [in type]
type [in type]
type' [in type']


U

unit [in unit]
unit [in unit]


Definition Index

A

Acc_intro' [in Acc_intro']
add [in add]
addLists [in addLists]
addLists' [in addLists']
All [in All]
allTrue [in allTrue]
app [in app]
app [in app]
app [in app]
append' [in append']
approx [in approx]
app' [in app']
asgn [in asgn]
a_b [in a_b]
a_star [in a_star]


B

backward [in backward]
bad [in bad]
balance1 [in balance1]
balance2 [in balance2]
bar [in bar]
Bind [in Bind]
binopDenote [in binopDenote]
bleh [in bleh]
bool_den [in bool_den]
bool_fix [in bool_fix]
bool_dt [in bool_dt]
boool [in boool]
Bottom [in Bottom]


C

cast [in cast]
cfold [in cfold]
cfold [in cfold]
cfoldCond [in cfoldCond]
check_even [in check_even]
choice_Set [in choice_Set]
compile [in compile]
computation [in computation]
comp_eq [in comp_eq]
cond [in cond]
conj' [in conj']
constructorDenote [in constructorDenote]
copies [in copies]
curriedAdd [in curriedAdd]
curriedAdd' [in curriedAdd']


D

datatype [in datatype]
datatypeDenote [in datatypeDenote]
datatypeDenoteOk [in datatypeDenoteOk]
dec_star' [in dec_star']
dec_star'' [in dec_star'']
dec_star [in dec_star]
deeeebug [in deeeebug]
depth [in depth]
doublePred [in doublePred]
doublePred' [in doublePred']


E

eapp [in eapp]
eir [in eir]
elength [in elength]
Empty_set_fix [in Empty_set_fix]
Empty_set_den [in Empty_set_den]
Empty_set_dt [in Empty_set_dt]
eq_type_dec [in eq_type_dec]
eq_nat_dec' [in eq_nat_dec']
eq_nat_dec [in eq_nat_dec]
er [in er]
eval [in eval]
eval [in eval]
evalExp [in evalExp]
eval1 [in eval1]
eval1' [in eval1']
eval1' [in eval1']
even_list_mut [in even_list_mut]
even_list_mut' [in even_list_mut']
existT' [in existT']
expDenote [in expDenote]
expDenote [in expDenote]
expDenote [in expDenote]
exp'Denote [in exp'Denote]
exp'Denote [in exp'Denote]
ex1 [in ex1]
e2u [in e2u]


F

fact [in fact]
fact_iter' [in fact_iter']
fact_slow' [in fact_slow']
fact_iter [in fact_iter]
fact_slow [in fact_slow]
falses_trues [in falses_trues]
False' [in False']
ffin [in ffin]
fget [in fget]
fhapp [in fhapp]
fhget [in fhget]
fhget [in fhget]
fhlist [in fhlist]
fhlist [in fhlist]
fhmap [in fhmap]
fi [in fi]
fib [in fib]
filist [in filist]
filter [in filter]
finOut [in finOut]
FirstOrder.add [in add]
FirstOrder.cfold [in cfold]
FirstOrder.ident [in ident]
FirstOrder.insertAt [in insertAt]
FirstOrder.insertAtS [in insertAtS]
FirstOrder.lift [in lift]
FirstOrder.liftVar [in liftVar]
FirstOrder.lift' [in lift']
FirstOrder.termDenote [in termDenote]
FirstOrder.three_the_hard_way [in three_the_hard_way]
FirstOrder.unlet [in unlet]
five_plus_three [in five_plus_three]
Fix [in Fix]
fixDenote [in fixDenote]
fixDenoteOk [in fixDenoteOk]
Fix' [in Fix']
flatten [in flatten]
fmember [in fmember]
fmember [in fmember]
foo [in foo]
foo [in foo]
foo [in foo]
foo [in foo]
Forall_c [in Forall_c]
forall_refl [in forall_refl]
formulaDenote [in formulaDenote]
formulaDenote [in formulaDenote]
formula_ind' [in formula_ind']
forward [in forward]
four_plus_three [in four_plus_three]
four_plus_three' [in four_plus_three']
frob [in frob]
frob [in frob]
frob' [in frob']
from_one_to_zero [in from_one_to_zero]


G

get [in get]
get [in get]
getNat [in getNat]
getNat' [in getNat']


H

hd [in hd]
hd [in hd]
hd' [in hd']
hget [in hget]
hi [in hi]
HigherOrder.Add [in Add]
HigherOrder.add [in add]
HigherOrder.add' [in add']
HigherOrder.Cfold [in Cfold]
HigherOrder.cfold [in cfold]
HigherOrder.countVars [in countVars]
HigherOrder.CountVars [in CountVars]
HigherOrder.Ident [in Ident]
HigherOrder.ident [in ident]
HigherOrder.pretty [in pretty]
HigherOrder.Pretty [in Pretty]
HigherOrder.squash [in squash]
HigherOrder.Subst [in Subst]
HigherOrder.Term [in Term]
HigherOrder.TermDenote [in TermDenote]
HigherOrder.termDenote [in termDenote]
HigherOrder.Term1 [in Term1]
HigherOrder.three_the_hard_way [in three_the_hard_way]
HigherOrder.three_the_hard_way' [in three_the_hard_way']
HigherOrder.Three_the_hard_way [in Three_the_hard_way]
HigherOrder.three_a_harder_way [in three_a_harder_way]
HigherOrder.unlet [in unlet]
HigherOrder.Unlet [in Unlet]
HigherOrder.Wf [in Wf]
holds [in holds]


I

id [in id]
id [in id]
id [in id]
id' [in id']
ifoldr [in ifoldr]
ilist [in ilist]
imap [in imap]
imap [in imap]
imp [in imp]
imp [in imp]
inc [in inc]
inc [in inc]
index_eq [in index_eq]
inject [in inject]
ins [in ins]
insert [in insert]
insert [in insert]
insertResult [in insertResult]
insResult [in insResult]
instrDenote [in instrDenote]
interleave [in interleave]
Int.f [in f]
Int.G [in G]
Int.i [in i]
Int.id [in id]
In_dec [in In_dec]
In_dec [in In_dec]
isZero [in isZero]


J

jme [in jme]
JMeq' [in JMeq']


L

lemma1' [in lemma1']
lemma2 [in lemma2]
lemma3' [in lemma3']
length [in length]
length [in length]
lengthOrder [in lengthOrder]
length_is_2 [in length_is_2]
length_is_2 [in length_is_2]
length_1_2 [in length_1_2]
length_and_sum [in length_and_sum]
length_and_sum'' [in length_and_sum'']
length_and_sum' [in length_and_sum']
leq [in leq]
list_fix [in list_fix]
list_nat_tree_ind [in list_nat_tree_ind]
list_dt [in list_dt]
list_den [in list_den]
looper [in looper]
looper [in looper]


M

makeRbtree [in makeRbtree]
map [in map]
map [in map]
map [in map]
map [in map]
map [in map]
mapp [in mapp]
map_nat [in map_nat]
map' [in map']
matches [in matches]
mdenote [in mdenote]
meq [in meq]
merge [in merge]
mergeSort [in mergeSort]
mergeSort' [in mergeSort']
mergeSort'' [in mergeSort'']
mldenote [in mldenote]
myNatIndex [in myNatIndex]
myTypes [in myTypes]
myValues [in myValues]
my_tauto [in my_tauto]


N

napp [in napp]
nat_tree_ind' [in nat_tree_ind']
nat_den [in nat_den]
nat_ind' [in nat_ind']
nat_dt [in nat_dt]
nat_fix [in nat_fix]
nat_rect' [in nat_rect']
needs_trans [in needs_trans]
negb [in negb]
negb' [in negb']
nlength [in nlength]
noot [in noot]
nsize [in nsize]
nsplice [in nsplice]
ntsize [in ntsize]
ntsplice [in ntsplice]
nvm [in nvm]


O

oapp [in oapp]
odd_list_mut [in odd_list_mut]
odd_list_mut' [in odd_list_mut']
olength [in olength]
ones [in ones]
ones' [in ones']
optCmd [in optCmd]
optExp [in optExp]


P

paartial [in paartial]
pairOut [in pairOut]
pairOutType [in pairOutType]
partialOut [in partialOut]
pformulaDenote [in pformulaDenote]
plus [in plus]
plus_recursive [in plus_recursive]
plus_rec [in plus_rec]
pred [in pred]
pred_strong1 [in pred_strong1]
pred_strong1 [in pred_strong1]
pred_strong2 [in pred_strong2]
pred_strong3 [in pred_strong3]
pred_strong4 [in pred_strong4]
pred_strong5 [in pred_strong5]
pred_strong6 [in pred_strong6]
pred_strong7 [in pred_strong7]
pred_strong8 [in pred_strong8]
pred_strong1' [in pred_strong1']
pred_strong4' [in pred_strong4']
pred_strong [in pred_strong]
pred' [in pred']
pred' [in pred']
present [in present]
present_insResult [in present_insResult]
print [in print]
print_datatype [in print_datatype]
print_nat [in print_nat]
prod' [in prod']
prog [in prog]
progDenote [in progDenote]
projE [in projE]
projS [in projS]
propify [in propify]


R

reassoc [in reassoc]
red_herring [in red_herring]
red_herring [in red_herring]
red_herring [in red_herring]
red_herring [in red_herring]
red_herring [in red_herring]
red_herring [in red_herring]
red_herring [in red_herring]
Return [in Return]
rifoldr [in rifoldr]
rpresent [in rpresent]
run [in run]
runTo [in runTo]


S

set [in set]
seven_minus_four [in seven_minus_four]
seven_minus_three'' [in seven_minus_three'']
seven_minus_three [in seven_minus_three]
seven_minus_three' [in seven_minus_three']
seven_minus_four' [in seven_minus_four']
seven_minus_four_zero [in seven_minus_four_zero]
seven_minus_four_zero [in seven_minus_four_zero]
seven_minus_three_again [in seven_minus_three_again]
size [in size]
skipCopies [in skipCopies]
somePairs [in somePairs]
someTypes [in someTypes]
someValues [in someValues]
split [in split]
split [in split]
split' [in split']
stack [in stack]
Streicher_K' [in Streicher_K']
sum [in sum]
sum [in sum]
sum [in sum]
sum [in sum]
sumboool [in sumboool]
swapper [in swapper]
syms [in syms]
sym_sig [in sym_sig]
sym_ex [in sym_ex]
synthesize1 [in synthesize1]
synthesize2 [in synthesize2]
synthesize3 [in synthesize3]


T

tautDenote [in tautDenote]
TBind [in TBind]
tbinopDenote [in tbinopDenote]
tcompile [in tcompile]
tconcat [in tconcat]
termDenote [in termDenote]
testCurriedAdd [in testCurriedAdd]
texpDenote [in texpDenote]
tg [in tg]
times [in times]
times [in times]
times [in times]
times [in times]
tinstrDenote [in tinstrDenote]
tl [in tl]
toProp [in toProp]
tprogDenote [in tprogDenote]
tree_den [in tree_den]
tree_fix [in tree_fix]
tree_dt [in tree_dt]
trues_falses [in trues_falses]
tstack [in tstack]
typeCheck [in typeCheck]
typeCheck' [in typeCheck']
typeDenote [in typeDenote]
typeDenote [in typeDenote]
typeDenote [in typeDenote]
typeDenote [in typeDenote]
typeDenote [in typeDenote]
types' [in types']
type'Denote [in type'Denote]


U

ugh [in ugh]
uhoh [in uhoh]
UIP_refl' [in UIP_refl']
unit_fix [in unit_fix]
unit_dt [in unit_dt]
unit_den [in unit_den]
unject [in unject]
update [in update]


V

var [in var]
vars [in vars]
vstack [in vstack]


Z

zeroes [in zeroes]
zero_minus_one [in zero_minus_one]


Axiom Index

C

classic [in classic]


G

GROUP_THEOREMS.inverse' [in inverse']
GROUP_THEOREMS.ident' [in ident']
GROUP_THEOREMS.unique_ident [in unique_ident]
GROUP.assoc [in assoc]
GROUP.f [in f]
GROUP.G [in G]
GROUP.i [in i]
GROUP.id [in id]
GROUP.ident [in ident]
GROUP.inverse [in inverse]


N

not_classic [in not_classic]
num [in num]


P

positive [in positive]


Module Index

C

Client [in Client]
Client.D [in Client.D]
Client.E [in Client.E]


F

FirstOrder [in FirstOrder]


G

GROUP [in GROUP]
GroupProofs [in GroupProofs]
GroupProofs.M [in GroupProofs.M]
GROUP_THEOREMS.M [in GROUP_THEOREMS.M]
GROUP_THEOREMS [in GROUP_THEOREMS]


H

HigherOrder [in HigherOrder]


I

Int [in Int]
IntProofs [in IntProofs]


L

Lib [in Lib]
Lib.A [in Lib.A]
Lib.B [in Lib.B]
Lib.C [in Lib.C]


Variable Index

A

All.P [in P]
All.T [in T]
autorewrite.A [in A]
autorewrite.f [in f]
autorewrite.f_f [in f_f]
autorewrite.garden_path.P [in P]
autorewrite.garden_path.P [in P]
autorewrite.garden_path.g [in g]
autorewrite.garden_path.g [in g]
autorewrite.garden_path.g [in g]
autorewrite.garden_path.f_g [in f_g]
autorewrite.garden_path.f_g [in f_g]
autorewrite.garden_path.f_g [in f_g]


B

Bind.A [in A]
Bind.B [in B]
Bind.m1 [in m1]
Bind.m2 [in m2]
Bottom.A [in A]


C

cfoldCond.default [in default]
cfoldCond.t [in t]
computation.A [in A]
cond.A [in A]
cond.default [in default]


D

dec_star.P [in P]
dec_star.dec_star''.n [in n]
dec_star.s [in s]
dec_star.P_dec [in P_dec]
dec_star.dec_star''.P'_dec [in P'_dec]
dec_star.dec_star''.P' [in P']
denote.T [in T]
depth.f [in f]


E

evalCmd_coind.R [in R]
evalCmd_coind.SeqCase [in SeqCase]
evalCmd_coind.AssignCase [in AssignCase]
evalCmd_coind.WhileCase [in WhileCase]
even_list_mut'.Podd [in Podd]
even_list_mut'.ECons_case [in ECons_case]
even_list_mut'.OCons_case [in OCons_case]
even_list_mut'.Peven [in Peven]
even_list_mut'.ENil_case [in ENil_case]


F

fhapp''.A [in A]
fhapp''.B [in B]
fhapp'.A [in A]
fhapp'.B [in B]
fhapp.A [in A]
fhapp.B [in B]
fhlist_map.A [in A]
fhlist_map.B [in B]
fhlist_map.C [in C]
fhlist_map.f [in f]
fhlist_map.elm [in elm]
fhlist.A [in A]
fhlist.A [in A]
fhlist.B [in B]
fhlist.B [in B]
fhlist.elm [in elm]
fhlist.elm [in elm]
filist.A [in A]
firstorder'.A [in A]
firstorder'.H1 [in H1]
firstorder'.H2 [in H2]
firstorder'.P [in P]
firstorder'.Q [in Q]
firstorder'.R [in R]
firstorder'.S [in S]
firstorder.A [in A]
firstorder.H1 [in H1]
firstorder.H2 [in H2]
firstorder.P [in P]
firstorder.Q [in Q]
firstorder.R [in R]
firstorder.S [in S]
Fix.A [in A]
Fix.B [in B]
Fix.f [in f]
Fix.f_continuous [in f_continuous]
forall_and.both [in both]
forall_and.A [in A]
forall_and.P [in P]
forall_and.Q [in Q]
Forall.A [in A]
Forall.P [in P]
Forall.P' [in P']
formula_ind'.P [in P]
formula_ind'.Eq_case [in Eq_case]
formula_ind'.And_case [in And_case]
formula_ind'.Forall_case [in Forall_case]


H

HigherOrder.var.var [in var]
HigherOrder.wf.var1 [in var1]
HigherOrder.wf.var2 [in var2]
hlist.A [in A]
hlist.B [in B]
hlist.elm [in elm]
hmap.A [in A]
hmap.B1 [in B1]
hmap.B2 [in B2]
hmap.B3 [in B3]
hmap.f1 [in f1]
hmap.f2 [in f2]


I

ifoldr.A [in A]
ifoldr.B [in B]
ifoldr.f [in f]
ifoldr.i [in i]
ilist_map.A [in A]
ilist_map.B [in B]
ilist_map.f [in f]
ilist.A [in A]
ilist.A [in A]
insert.present.z [in z]
insert.x [in x]
interleave.A [in A]
In_dec.A [in A]
In_dec.A_eq_dec [in A_eq_dec]


L

lattice.A [in A]
list.T [in T]


M

map'.A [in A]
map'.B [in B]
map'.f [in f]
map.A [in A]
map.B [in B]
map.F [in F]
map.f [in f]
map.T [in T]
map.T' [in T']
mergeSort.A [in A]
mergeSort.le [in le]
monoid.A [in A]
monoid.assoc [in assoc]
monoid.e [in e]
monoid.f [in f]
monoid.identl [in identl]
monoid.identr [in identr]
my_tauto.atomics [in atomics]


N

nat_tree_ind'.P [in P]
nat_ind'.P [in P]
nat_tree_ind'.NNode'_case [in NNode'_case]
nat_ind'.S_case [in S_case]
nat_ind'.O_case [in O_case]


O

ok.dd [in dd]
ok.dt [in dt]
ok.fx [in fx]
ok.T [in T]


P

present.x [in x]
propositional.P [in P]
Propositional.P [in P]
propositional.Q [in Q]
Propositional.Q [in Q]
propositional.R [in R]
Propositional.R [in R]


R

Return.A [in A]
Return.v [in v]
rifoldr.A [in A]
rifoldr.B [in B]
rifoldr.f [in f]
rifoldr.i [in i]


S

slow.A [in A]
slow.f [in f]
slow.H1 [in H1]
slow.H2 [in H2]
slow.H3 [in H3]
slow.P [in P]
slow.Q [in Q]
slow.R [in R]
slow.S [in S]
split.P1 [in P1]
split.P1_dec [in P1_dec]
split.P2 [in P2]
split.P2_dec [in P2_dec]
split.s [in s]
star.P [in P]
stream_eq_onequant.Cons_case_hd [in Cons_case_hd]
stream_eq_loop.Cons_case_hd [in Cons_case_hd]
stream_eq_coind.Cons_case_hd [in Cons_case_hd]
stream_eq_onequant.A [in A]
stream_eq_loop.A [in A]
stream_eq_coind.A [in A]
stream_eq.A [in A]
stream_eq_onequant.B [in B]
stream_eq_coind.R [in R]
stream_eq_onequant.f [in f]
stream_eq_onequant.g [in g]
stream_eq_onequant.Cons_case_tl [in Cons_case_tl]
stream_eq_coind.Cons_case_tl [in Cons_case_tl]
stream_eq_loop.s1 [in s1]
stream_eq_loop.s2 [in s2]
stream_eq_loop.loop1 [in loop1]
stream_eq_loop.loop2 [in loop2]
stream.A [in A]


T

test_inster.A [in A]
test_inster.P [in P]
test_inster.Q [in Q]
test_inster.f [in f]
test_inster.g [in g]
test_inster.H1 [in H1]
test_inster.H3 [in H3]
test_inster.H4 [in H4]
thunk_eq_coind.A [in A]
thunk_eq_coind.H [in H]
thunk_eq_coind.P [in P]
tree.A [in A]
tree.A [in A]
tree.A [in A]
twoEls.A [in A]
t6.A [in A]
t6.B [in B]
t6.f [in f]
t6.g [in g]
t6.H1 [in H1]
t6.H2 [in H2]
t6.P [in P]
t7.A [in A]
t7.A [in A]
t7.B [in B]
t7.B [in B]
t7.f [in f]
t7.f [in f]
t7.g [in g]
t7.g [in g]
t7.H1 [in H1]
t7.H1 [in H1]
t7.H2 [in H2]
t7.H2 [in H2]
t7.P [in P]
t7.P [in P]
t7.Q [in Q]
t7.Q [in Q]


W

withTypes'.natIndex [in natIndex]
withTypes'.types [in types]
withTypes'.values [in values]
withTypes.natIndex [in natIndex]
withTypes.natIndex_ok [in natIndex_ok]
withTypes.types [in types]
withTypes.values [in values]


Library Index

C

Coinductive
Conclusion


D

DataStruct


E

Equality


G

GeneralRec
Generic


I

InductiveTypes
Intro


L

Large
LogicProg


M

Match
MoreDep


P

Predicates
ProgLang


R

Reflection


S

StackMachine
Subset


U

Universes


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 _ other (1484 entries)
Projection 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 _ other (7 entries)
Record 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 _ other (3 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 _ other (354 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 _ other (77 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 _ other (245 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 _ other (33 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 _ other (99 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 _ other (385 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 _ other (14 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 _ other (16 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 _ other (233 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 _ other (18 entries)
This page has been generated by coqdoc