Global Index

other

(1280 entries)

Projection Index

other

(4 entries)

Record Index

other

(2 entries)

Lemma Index

other

(328 entries)

Section Index

other

(70 entries)

Constructor Index

other

(217 entries)

Notation Index

other

(30 entries)

Inductive Index

other

(90 entries)

Definition Index

other

(286 entries)

Module Index

other

(7 entries)

Axiom Index

other

(15 entries)

Variable Index

other

(215 entries)

Library Index

other

(16 entries)

Global Index

A

B

backward [definition, in Reflection]
balanced [lemma, in MoreDep]
balance1 [definition, in MoreDep]
balance2 [definition, in MoreDep]
Bar [constructor, in Universes]
bar [inductive, in Universes]
Base [constructor, in Universes]
BConst [constructor, in MoreDep]
BConst [constructor, in DataStruct]
Bind [definition, in GeneralRec]
Bind [section, in GeneralRec]
Bind.A [variable, in GeneralRec]
Bind.B [variable, in GeneralRec]
Bind.m1 [variable, in GeneralRec]
Bind.m2 [variable, in GeneralRec]
binop [inductive, in StackMachine]
Binop [constructor, in StackMachine]
binopDenote [definition, in StackMachine]
Black [constructor, in MoreDep]
BlackNode [constructor, in MoreDep]
Bnd [constructor, in GeneralRec]
Bool [constructor, in Subset]
Bool [constructor, in StackMachine]
bool [inductive, in Predicates]
bool [inductive, in InductiveTypes]
Bool [constructor, in MoreDep]
Bool [constructor, in DataStruct]
bool_neq [lemma, in LogicProg]
bool_neq [lemma, in LogicProg]
bool_fix [definition, in Generic]
bool_den [definition, in Generic]
bool_dt [definition, in Generic]
Bottom [definition, in GeneralRec]
Bottom [section, in GeneralRec]
Bottom.A [variable, in GeneralRec]

C

cassociativity [lemma, in GeneralRec]
cassociativity1 [lemma, in GeneralRec]
cassociativity2 [lemma, in GeneralRec]
cast [definition, in Universes]
cfold [definition, in MoreDep]
cfold [definition, in DataStruct]
cfoldCond [section, in DataStruct]
cfoldCond [definition, in DataStruct]
cfoldCond_correct [lemma, in DataStruct]
cfoldCond.default [variable, in DataStruct]
cfoldCond.t [variable, in DataStruct]
cfold_correct [lemma, in DataStruct]
cfold_correct [lemma, in Large]
cfold_correct [lemma, in Large]
cfold_correct [lemma, in Large]
cfold_correct [lemma, in MoreDep]
ChainCons [constructor, in GeneralRec]
Char [constructor, in MoreDep]
check_even [definition, in Reflection]
choice_Set [definition, in Universes]
classic [axiom, in Universes]
cleft_identity [lemma, in GeneralRec]
cmd [inductive, in Coinductive]
Coinductive [library]
color [inductive, in MoreDep]
combine [lemma, in LogicProg]
comm_conc [lemma, in Match]
comm_prem [lemma, in Match]
comp [inductive, in GeneralRec]
compile [definition, in StackMachine]
compile_correct [lemma, in StackMachine]
compile_correct' [lemma, in StackMachine]
compile_correct [lemma, in StackMachine]
compile_correct' [lemma, in StackMachine]
computation [section, in GeneralRec]
computation [definition, in GeneralRec]
computation.A [variable, in GeneralRec]
comp_eq [definition, in GeneralRec]
Con [constructor, in Generic]
Concat [constructor, in MoreDep]
Cond [constructor, in DataStruct]
cond [section, in DataStruct]
cond [definition, in DataStruct]
cond_ext [lemma, in DataStruct]
cond.A [variable, in DataStruct]
cond.default [variable, in DataStruct]
confounder [lemma, in Large]
conj [constructor, in Predicates]
Conjunction [constructor, in InductiveTypes]
Cons [constructor, in InductiveTypes]
Cons [constructor, in InductiveTypes]
Cons [constructor, in DataStruct]
Cons [constructor, in Coinductive]
Cons [constructor, in MoreDep]
Const [constructor, in LogicProg]
Const [constructor, in Universes]
Const [constructor, in DataStruct]
Const [constructor, in Coinductive]
Const [constructor, in Large]
Const [constructor, in Large]
Const [constructor, in StackMachine]
ConstP [constructor, in Universes]
constructor [record, in Generic]
constructorDenote [definition, in Generic]
contra [lemma, in Predicates]
cright_identity [lemma, in GeneralRec]
curriedAdd [definition, in GeneralRec]
curriedAdd' [definition, in GeneralRec]

D

E

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

F

f [variable, in LogicProg]
fact [definition, in GeneralRec]
fact_eq' [lemma, in Coinductive]
fact_eq [lemma, in Coinductive]
fact_def [lemma, in Coinductive]
fact_slow [definition, in Coinductive]
fact_iter' [definition, in Coinductive]
fact_iter [definition, in Coinductive]
fact_slow' [definition, in Coinductive]
fact_eq'' [lemma, in Coinductive]
Fals [constructor, in Predicates]
false [constructor, in Predicates]
false [constructor, in InductiveTypes]
falseFree [inductive, in Predicates]
falseFree_holds [lemma, in Predicates]
Falsehood [constructor, in Reflection]
Falsehood [constructor, in InductiveTypes]
Falsehood' [constructor, in Reflection]
falses_trues [definition, in Coinductive]
False_imp [lemma, in Predicates]
False_prem [lemma, in Match]
FFAnd [constructor, in Predicates]
ffin [definition, in DataStruct]
FFNot [constructor, in Predicates]
FFTru [constructor, in Predicates]
fget [definition, in DataStruct]
fhapp [section, in Equality]
fhapp [definition, in Equality]
fhapp_ass' [lemma, in Equality]
fhapp_ass [lemma, in Equality]
fhapp' [section, in Equality]
fhapp'.A [variable, in Equality]
fhapp'.B [variable, in Equality]
fhapp.A [variable, in Equality]
fhapp.B [variable, in Equality]
fhget [definition, in Equality]
fhget [definition, in DataStruct]
fhlist [section, in Equality]
fhlist [section, in DataStruct]
fhlist [definition, in DataStruct]
fhlist [definition, in Equality]
fhlist_map.C [variable, in Equality]
fhlist_map.elm [variable, in Equality]
fhlist_map.A [variable, in Equality]
fhlist_map.B [variable, in Equality]
fhlist_map.f [variable, in Equality]
fhlist_map [section, in Equality]
fhlist.A [variable, in DataStruct]
fhlist.A [variable, in Equality]
fhlist.B [variable, in Equality]
fhlist.B [variable, in DataStruct]
fhlist.elm [variable, in DataStruct]
fhlist.elm [variable, in Equality]
fhmap [definition, in Equality]
filist [definition, in DataStruct]
filist [section, in DataStruct]
filist.A [variable, in DataStruct]
fin [inductive, in DataStruct]
finOut [definition, in Universes]
fin_cases_again [lemma, in Universes]
fin_cases [lemma, in Universes]
fin_cases_again' [lemma, in Universes]
First [constructor, in DataStruct]
firstorder [section, in Match]
firstorder' [section, in Match]
firstorder'.A [variable, in Match]
firstorder'.H1 [variable, in Match]
firstorder'.H2 [variable, in Match]
firstorder'.P [variable, in Match]
firstorder'.Q [variable, in Match]
firstorder'.R [variable, in Match]
firstorder'.S [variable, in Match]
firstorder.A [variable, in Match]
firstorder.H1 [variable, in Match]
firstorder.H2 [variable, in Match]
firstorder.P [variable, in Match]
firstorder.Q [variable, in Match]
firstorder.R [variable, in Match]
firstorder.S [variable, in Match]
five_plus_three' [definition, in LogicProg]
Fix [section, in GeneralRec]
Fix [definition, in GeneralRec]
fixDenote [definition, in Generic]
fixDenoteOk [definition, in Generic]
Fix' [definition, in GeneralRec]
Fix'_ok [lemma, in GeneralRec]
Fix.A [variable, in GeneralRec]
Fix.B [variable, in GeneralRec]
Fix.f [variable, in GeneralRec]
Fix.f_continuous [variable, in GeneralRec]
flatten [definition, in Reflection]
flatten_correct [lemma, in Reflection]
flatten_correct' [lemma, in Reflection]
fmember [definition, in Equality]
fmember [definition, in DataStruct]
fo [lemma, in Match]
foldr_plus [lemma, in Generic]
foo [inductive, in Universes]
Foo [constructor, in Universes]
Forall [constructor, in Universes]
Forall [constructor, in InductiveTypes]
forall_and.A [variable, in LogicProg]
forall_exists_commute [lemma, in Predicates]
forall_refl [definition, in InductiveTypes]
forall_and [lemma, in LogicProg]
forall_and [section, in LogicProg]
forall_eq [lemma, in Equality]
forall_and.both [variable, in LogicProg]
forall_and.P [variable, in LogicProg]
forall_and.Q [variable, in LogicProg]
formula [inductive, in InductiveTypes]
formula [inductive, in Reflection]
formula [inductive, in Universes]
formulaDenote [definition, in InductiveTypes]
formulaDenote [definition, in Reflection]
formula_ind' [definition, in InductiveTypes]
formula_ind'.Eq_case [variable, in InductiveTypes]
formula_ind' [section, in InductiveTypes]
formula_ind'.Forall_case [variable, in InductiveTypes]
formula_ind'.And_case [variable, in InductiveTypes]
formula_ind'.P [variable, in InductiveTypes]
formula' [inductive, in Reflection]
forward [definition, in Reflection]
Found [constructor, in Subset]
four_plus_three [definition, in LogicProg]
four_plus_three' [definition, in LogicProg]
fo' [lemma, in Match]
frob [definition, in Coinductive]
frob [definition, in GeneralRec]
frob_eq [lemma, in Coinductive]
frob_eq [lemma, in GeneralRec]
frob' [definition, in GeneralRec]
Fst [constructor, in MoreDep]
Func [constructor, in Universes]
f_f_f [lemma, in LogicProg]
f_f_f' [lemma, in LogicProg]
f_f_f' [lemma, in LogicProg]
f_f_f' [lemma, in LogicProg]
f_f_f_g [lemma, in LogicProg]

G

G [variable, in LogicProg]
GeneralRec [library]
Generic [library]
get [definition, in DataStruct]
get_imap [lemma, in DataStruct]
get_imap [lemma, in Equality]
ge_refl [lemma, in GeneralRec]
Group [module, in Large]
GROUP [module, in Large]
GROUP_THEOREMS.M [module, in Large]
GROUP_THEOREMS.ident' [axiom, in Large]
GROUP_THEOREMS [module, in Large]
GROUP_THEOREMS.unique_ident [axiom, in Large]
GROUP_THEOREMS.inverse' [axiom, in Large]
GROUP.assoc [axiom, in Large]
GROUP.e [axiom, in Large]
GROUP.f [axiom, in Large]
GROUP.G [axiom, in Large]
GROUP.i [axiom, in Large]
GROUP.ident [axiom, in Large]
Group.ident' [lemma, in Large]
GROUP.inverse [axiom, in Large]
Group.inverse' [lemma, in Large]
Group.M [module, in Large]
Group.unique_ident [lemma, in Large]

H

HAnd [constructor, in Predicates]
HAnd' [constructor, in Predicates]
hasType [inductive, in Subset]
hasType_det [lemma, in Subset]
hd [definition, in MoreDep]
hd [definition, in Coinductive]
hd' [definition, in MoreDep]
hget [definition, in DataStruct]
hi [definition, in MoreDep]
hlist [inductive, in DataStruct]
hlist [section, in DataStruct]
hlist.A [variable, in DataStruct]
hlist.B [variable, in DataStruct]
hlist.elm [variable, in DataStruct]
hmm [lemma, in Match]
hmm' [lemma, in Match]
hmm2 [lemma, in Match]
holds [definition, in Reflection]
holds [inductive, in Predicates]
holds' [inductive, in Predicates]
HOr1 [constructor, in Predicates]
HOr1' [constructor, in Predicates]
HOr2 [constructor, in Predicates]
HOr2' [constructor, in Predicates]
HtAnd [constructor, in Subset]
HtBool [constructor, in Subset]
HtNat [constructor, in Subset]
HtPlus [constructor, in Subset]
HTru [constructor, in Predicates]
HTru' [constructor, in Predicates]
hundred_minus_hundred [definition, in LogicProg]

I

iBinop [constructor, in StackMachine]
iConst [constructor, in StackMachine]
id [definition, in Universes]
id [definition, in Universes]
id [definition, in Equality]
Ident [constructor, in Reflection]
id' [definition, in Equality]
If [constructor, in MoreDep]
ifoldr [definition, in DataStruct]
ifoldr [section, in DataStruct]
ifoldr.A [variable, in DataStruct]
ifoldr.B [variable, in DataStruct]
ifoldr.f [variable, in DataStruct]
ifoldr.i [variable, in DataStruct]
ilist [section, in MoreDep]
ilist [inductive, in MoreDep]
ilist [inductive, in DataStruct]
ilist [section, in DataStruct]
ilist_map.f [variable, in DataStruct]
ilist_map.B [variable, in DataStruct]
ilist_map.A [variable, in DataStruct]
ilist_map [section, in DataStruct]
ilist.A [variable, in MoreDep]
ilist.A [variable, in DataStruct]
imap [definition, in DataStruct]
Imp [constructor, in Reflection]
imp [definition, in Match]
imp [definition, in Reflection]
imp_True [lemma, in Match]
Imp' [constructor, in Reflection]
inc [definition, in DataStruct]
inc [definition, in DataStruct]
index_eq [definition, in Reflection]
InductiveTypes [library]
Inject [constructor, in Universes]
inject [definition, in MoreDep]
inject_inverse [lemma, in MoreDep]
ins [definition, in MoreDep]
insert [section, in MoreDep]
insert [definition, in GeneralRec]
insert [definition, in MoreDep]
insertResult [definition, in MoreDep]
insert.present [section, in MoreDep]
insert.present.z [variable, in MoreDep]
insert.x [variable, in MoreDep]
insResult [definition, in MoreDep]
instr [inductive, in StackMachine]
instrDenote [definition, in StackMachine]
Int [module, in Large]
interleave [section, in Coinductive]
interleave [definition, in Coinductive]
interleave.A [variable, in Coinductive]
Intro [library]
IntTheorems [module, in Large]
Int.assoc [lemma, in Large]
Int.e [definition, in Large]
Int.f [definition, in Large]
Int.G [definition, in Large]
Int.i [definition, in Large]
Int.ident [lemma, in Large]
Int.inverse [lemma, in Large]
In_dec [definition, in Subset]
in_star [lemma, in LogicProg]
In_dec.A [variable, in Subset]
In_dec [definition, in Reflection]
In_dec [section, in Subset]
In_dec.A_eq_dec [variable, in Subset]
isChain [inductive, in GeneralRec]
isEven [inductive, in Reflection]
isZero [definition, in InductiveTypes]
IsZero [constructor, in Predicates]
isZero [inductive, in Predicates]
isZero_contra [lemma, in Predicates]
isZero_contra' [lemma, in Predicates]
isZero_zero [lemma, in Predicates]
isZero_plus [lemma, in Predicates]
Iter [constructor, in MoreDep]

J

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

L

Large [library]
lattice [section, in GeneralRec]
lattice.A [variable, in GeneralRec]
Leaf [constructor, in DataStruct]
Leaf [constructor, in Generic]
Leaf [constructor, in MoreDep]
Leaf [constructor, in DataStruct]
left_identity [lemma, in GeneralRec]
lemma1 [lemma, in Equality]
lemma1' [definition, in Equality]
lemma2 [definition, in Equality]
lemma2 [lemma, in Equality]
lemma3 [lemma, in Equality]
lemma3 [lemma, in Equality]
lemma4 [lemma, in Equality]
length [definition, in InductiveTypes]
length [definition, in InductiveTypes]
lengthOrder [definition, in GeneralRec]
lengthOrder_wf' [lemma, in GeneralRec]
lengthOrder_wf [lemma, in GeneralRec]
length_1_2 [definition, in LogicProg]
length_and_sum'' [definition, in LogicProg]
length_emp [lemma, in MoreDep]
length_O [lemma, in LogicProg]
length_and_sum' [definition, in LogicProg]
length_app [lemma, in InductiveTypes]
length_app [lemma, in InductiveTypes]
length_is_2 [definition, in LogicProg]
length_is_2 [definition, in LogicProg]
length_app1 [lemma, in MoreDep]
length_S [lemma, in LogicProg]
length_and_sum [definition, in LogicProg]
leq [definition, in GeneralRec]
leq_None [lemma, in GeneralRec]
leq_Some [lemma, in GeneralRec]
Lift [constructor, in Universes]
linear [lemma, in LogicProg]
list [inductive, in InductiveTypes]
list [section, in InductiveTypes]
list [inductive, in InductiveTypes]
list_fix [definition, in Generic]
list_dt [definition, in Generic]
list_den [definition, in Generic]
list.T [variable, in InductiveTypes]
LogicProg [library]
looper [definition, in GeneralRec]

M

makeRbtree [definition, in MoreDep]
map [definition, in GeneralRec]
map [section, in InductiveTypes]
map [definition, in Coinductive]
map [definition, in InductiveTypes]
map [definition, in Generic]
map [section, in Coinductive]
map_id [lemma, in Generic]
map_nat [definition, in Generic]
map' [section, in Coinductive]
map'.A [variable, in Coinductive]
map'.B [variable, in Coinductive]
map'.f [variable, in Coinductive]
map.A [variable, in Coinductive]
map.B [variable, in Coinductive]
map.F [variable, in InductiveTypes]
map.f [variable, in Coinductive]
map.T [variable, in InductiveTypes]
map.T' [variable, in InductiveTypes]
Match [lemma, in Match]
Match [library]
matches [definition, in MoreDep]
max_1 [lemma, in GeneralRec]
max_2 [lemma, in GeneralRec]
maybe [inductive, in Subset]
MCons [constructor, in DataStruct]
mdenote [definition, in Reflection]
member [inductive, in DataStruct]
meq [definition, in GeneralRec]
merge [definition, in GeneralRec]
mergeSort [section, in GeneralRec]
mergeSort [definition, in GeneralRec]
mergeSort_eq [lemma, in GeneralRec]
mergeSort' [definition, in GeneralRec]
mergeSort'' [definition, in GeneralRec]
mergeSort.A [variable, in GeneralRec]
mergeSort.le [variable, in GeneralRec]
mexp [inductive, in Reflection]
MFirst [constructor, in DataStruct]
minus_minus [lemma, in MoreDep]
mldenote [definition, in Reflection]
MNext [constructor, in DataStruct]
MNil [constructor, in DataStruct]
monoid [section, in Reflection]
monoid_reflect [lemma, in Reflection]
monoid.A [variable, in Reflection]
monoid.assoc [variable, in Reflection]
monoid.e [variable, in Reflection]
monoid.f [variable, in Reflection]
monoid.identl [variable, in Reflection]
monoid.identr [variable, in Reflection]
_ + _ [notation, in Reflection]
MoreDep [library]
mt1 [lemma, in Reflection]
mt2 [lemma, in Reflection]
mt3 [lemma, in Reflection]
mt3' [lemma, in Reflection]
mt4 [lemma, in Reflection]
mt4' [lemma, in Reflection]
Mult [constructor, in Large]
mult_both [lemma, in LogicProg]
my_tauto [section, in Reflection]
my_tauto [definition, in Reflection]
my_tauto.atomics [variable, in Reflection]
m1 [lemma, in Match]
m2 [lemma, in Match]

N

O

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

P

Pair [constructor, in Universes]
Pair [constructor, in MoreDep]
pairOut [definition, in MoreDep]
pairOutDefault [definition, in MoreDep]
pairOutType [definition, in MoreDep]
PairP [constructor, in Universes]
pair' [constructor, in Universes]
PAnd [constructor, in Universes]
partialOut [definition, in Reflection]
partition [definition, in GeneralRec]
partition_wf1 [lemma, in GeneralRec]
partition_wf2 [lemma, in GeneralRec]
partition_wf [lemma, in GeneralRec]
pformula [inductive, in InductiveTypes]
pformulaDenote [definition, in InductiveTypes]
PI [constructor, in Generic]
PInject [constructor, in Universes]
Plus [constructor, in MoreDep]
Plus [constructor, in Coinductive]
Plus [constructor, in LogicProg]
Plus [constructor, in Large]
Plus [constructor, in Large]
Plus [constructor, in Subset]
plus [definition, in InductiveTypes]
Plus [constructor, in DataStruct]
Plus [constructor, in StackMachine]
PlusO [constructor, in LogicProg]
plusO [lemma, in LogicProg]
plusO' [lemma, in LogicProg]
plusR [inductive, in LogicProg]
plusR_plus [lemma, in LogicProg]
PlusS [constructor, in LogicProg]
plusS [lemma, in LogicProg]
plus_plusR [lemma, in LogicProg]
plus_ge [lemma, in DataStruct]
plus_n_Sm' [lemma, in MoreDep]
plus_assoc [lemma, in InductiveTypes]
plus_0 [lemma, in LogicProg]
plus_S [lemma, in InductiveTypes]
plus1 [lemma, in Universes]
positive [axiom, in Universes]
pred [definition, in InductiveTypes]
Predicates [library]
predicate_extensionality [lemma, in Universes]
pred_strong7 [definition, in Subset]
pred_strong5 [definition, in Subset]
pred_strong1_irrel [lemma, in Universes]
pred_strong4' [definition, in Subset]
pred_strong3 [definition, in Subset]
pred_strong1 [definition, in Subset]
pred_strong8 [definition, in Subset]
pred_strong2 [definition, in Subset]
pred_strong1_irrel' [lemma, in Universes]
pred_strong6 [definition, in Subset]
pred_strong4 [definition, in Subset]
pred_strong1' [definition, in Subset]
pred_strong1 [definition, in Universes]
pred' [definition, in Equality]
present [section, in MoreDep]
present [definition, in MoreDep]
present_insResult [definition, in MoreDep]
present_insert_Black [lemma, in MoreDep]
present_balance1 [lemma, in MoreDep]
present_insert_Red [lemma, in MoreDep]
present_balance2 [lemma, in MoreDep]
present_ins [lemma, in MoreDep]
present.x [variable, in MoreDep]
print [definition, in Generic]
printName [projection, in Generic]
printNonrec [projection, in Generic]
print_datatype [definition, in Generic]
print_constructor [record, in Generic]
print_nat [definition, in Generic]
prod [inductive, in Predicates]
Prod [constructor, in MoreDep]
prod' [inductive, in Universes]
prog [definition, in StackMachine]
progDenote [definition, in StackMachine]
projS [definition, in Universes]
proj1 [lemma, in Universes]
proj1_again'' [lemma, in Universes]
proj1_again' [lemma, in Universes]
proj1_again [lemma, in Universes]
proof [inductive, in Universes]
prop [inductive, in Predicates]
propify [definition, in Predicates]
propify_holds [lemma, in Predicates]
propify_holds' [lemma, in Predicates]
Propositional [section, in Predicates]
propositional [section, in Match]
propositional [lemma, in Match]
Propositional.P [variable, in Predicates]
propositional.P [variable, in Match]
propositional.Q [variable, in Match]
Propositional.Q [variable, in Predicates]
propositional.R [variable, in Match]
Propositional.R [variable, in Predicates]
prop' [inductive, in Predicates]

R

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

S

T

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

U

uhoh [lemma, in Universes]
uhoh_again [lemma, in Universes]
UIP [lemma, in Universes]
UIP_refl' [definition, in Equality]
UIP_refl'' [lemma, in Equality]
UIP_refl [lemma, in Universes]
unique_ident [lemma, in Large]
Unit [constructor, in DataStruct]
unit [inductive, in Predicates]
unit [inductive, in InductiveTypes]
unit_den [definition, in Generic]
unit_fix [definition, in Generic]
unit_dt [definition, in Generic]
unit_singleton [lemma, in InductiveTypes]
unit_rect' [definition, in InductiveTypes]
Universes [library]
unject [definition, in MoreDep]
Unknown [constructor, in Subset]

V

Var [constructor, in Coinductive]
Var [constructor, in Reflection]
var [definition, in Coinductive]
Var [constructor, in DataStruct]
Var [constructor, in LogicProg]
VarEq [constructor, in Universes]
vars [definition, in Coinductive]
vstack [definition, in StackMachine]

W

While [constructor, in Coinductive]

Z

zeroes [definition, in Coinductive]
zero_times [lemma, in LogicProg]
zgtz [lemma, in Universes]
zgtz [lemma, in Subset]

other

_ --> _ [notation, in Reflection]
_ --> _ [notation, in Match]
_ ;;; _ [notation, in Subset]
_ * _ [notation, in LogicProg]
_ ;; _ [notation, in Subset]
_ <- _ ; _ [notation, in GeneralRec]
_ <- _ ; _ [notation, in GeneralRec]
_ === _ [notation, in Equality]
_ <- _ ; _ [notation, in Subset]
_ <- _ ; _ [notation, in GeneralRec]
_ || _ [notation, in Subset]
_ == _ [notation, in Equality]
_ <-- _ ; _ [notation, in Subset]
No [notation, in Subset]
Reduce _ [notation, in Subset]
Yes [notation, in Subset]
!! [notation, in Subset]
! [notation, in Subset]
?? [notation, in Subset]
[ ! , _ ~> _ ] [notation, in Generic]
[ ! , ! ~> _ ] [notation, in Generic]
[ _ , _ ~> _ ] [notation, in Generic]
[ _ ] [notation, in Subset]
[ _ , ! ~> _ ] [notation, in Generic]
[| _ |] [notation, in Subset]
[|| _ ||] [notation, in Subset]
^ [notation, in Generic]
{< _ >} [notation, in MoreDep]
{{ _ | _ }} [notation, in Subset]

Projection Index

N

nonrecursive [in Generic]

P

printName [in Generic]
printNonrec [in Generic]

R

recursive [in Generic]

Record Index

C

constructor [in Generic]

P

print_constructor [in Generic]

Lemma Index

A

allTrue_In [in Reflection]
allTrue_add [in Reflection]
and_comm [in Predicates]
and_assoc [in Predicates]
and_True_conc [in Match]
and_True_prem [in Match]
append_emp [in MoreDep]
app_empty_end [in MoreDep]
app_cong [in MoreDep]
arith_comm [in Predicates]
arith_neq [in Predicates]
arith_neq' [in Predicates]
arith_comm' [in Predicates]
associativity [in GeneralRec]
assoc_prem1 [in Match]
assoc_conc1 [in Match]
assoc_prem2 [in Match]
assoc_conc2 [in Match]

B

balanced [in MoreDep]
bool_neq [in LogicProg]
bool_neq [in LogicProg]

C

cassociativity [in GeneralRec]
cassociativity1 [in GeneralRec]
cassociativity2 [in GeneralRec]
cfoldCond_correct [in DataStruct]
cfold_correct [in DataStruct]
cfold_correct [in Large]
cfold_correct [in Large]
cfold_correct [in Large]
cfold_correct [in MoreDep]
cleft_identity [in GeneralRec]
combine [in LogicProg]
comm_conc [in Match]
comm_prem [in Match]
compile_correct [in StackMachine]
compile_correct' [in StackMachine]
compile_correct [in StackMachine]
compile_correct' [in StackMachine]
cond_ext [in DataStruct]
confounder [in Large]
contra [in Predicates]
cright_identity [in GeneralRec]

D

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

E

F

fact_eq' [in Coinductive]
fact_eq [in Coinductive]
fact_def [in Coinductive]
fact_eq'' [in Coinductive]
falseFree_holds [in Predicates]
False_imp [in Predicates]
False_prem [in Match]
fhapp_ass' [in Equality]
fhapp_ass [in Equality]
fin_cases_again [in Universes]
fin_cases [in Universes]
fin_cases_again' [in Universes]
Fix'_ok [in GeneralRec]
flatten_correct [in Reflection]
flatten_correct' [in Reflection]
fo [in Match]
foldr_plus [in Generic]
forall_exists_commute [in Predicates]
forall_and [in LogicProg]
forall_eq [in Equality]
fo' [in Match]
frob_eq [in Coinductive]
frob_eq [in GeneralRec]
f_f_f [in LogicProg]
f_f_f' [in LogicProg]
f_f_f' [in LogicProg]
f_f_f' [in LogicProg]
f_f_f_g [in LogicProg]

G

get_imap [in DataStruct]
get_imap [in Equality]
ge_refl [in GeneralRec]
Group.ident' [in Large]
Group.inverse' [in Large]
Group.unique_ident [in Large]

H

hasType_det [in Subset]
hmm [in Match]
hmm' [in Match]
hmm2 [in Match]

I

imp_True [in Match]
inject_inverse [in MoreDep]
Int.assoc [in Large]
Int.ident [in Large]
Int.inverse [in Large]
in_star [in LogicProg]
isZero_contra [in Predicates]
isZero_contra' [in Predicates]
isZero_zero [in Predicates]
isZero_plus [in Predicates]

J

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

L

left_identity [in GeneralRec]
lemma1 [in Equality]
lemma2 [in Equality]
lemma3 [in Equality]
lemma3 [in Equality]
lemma4 [in Equality]
lengthOrder_wf' [in GeneralRec]
lengthOrder_wf [in GeneralRec]
length_emp [in MoreDep]
length_O [in LogicProg]
length_app [in InductiveTypes]
length_app [in InductiveTypes]
length_app1 [in MoreDep]
length_S [in LogicProg]
leq_None [in GeneralRec]
leq_Some [in GeneralRec]
linear [in LogicProg]

M

map_id [in Generic]
Match [in Match]
max_1 [in GeneralRec]
max_2 [in GeneralRec]
mergeSort_eq [in GeneralRec]
minus_minus [in MoreDep]
monoid_reflect [in Reflection]
mt1 [in Reflection]
mt2 [in Reflection]
mt3 [in Reflection]
mt3' [in Reflection]
mt4 [in Reflection]
mt4' [in Reflection]
mult_both [in LogicProg]
m1 [in Match]
m2 [in Match]

N

nat_eq_dec [in Universes]
negb_inverse [in InductiveTypes]
negb_ineq [in InductiveTypes]
nlength_napp [in InductiveTypes]
noChains [in GeneralRec]
noChains' [in GeneralRec]
nsize_nsplice [in InductiveTypes]
ntsize_ntsplice [in InductiveTypes]
n_plus_O' [in InductiveTypes]
n_plus_O [in InductiveTypes]

O

obvious [in Predicates]
obvious' [in Predicates]
ones_eq [in Coinductive]
ones_eq''' [in Coinductive]
ones_eq' [in Coinductive]
ones_eq [in Coinductive]
ones_eq [in Coinductive]
ones_eq'' [in Coinductive]
optCmd_correct [in Coinductive]
optExp_correct [in Coinductive]
or_assoc [in Predicates]
or_comm' [in Predicates]
or_comm [in Predicates]
O_plus_n [in InductiveTypes]

P

partition_wf1 [in GeneralRec]
partition_wf2 [in GeneralRec]
partition_wf [in GeneralRec]
plusO [in LogicProg]
plusO' [in LogicProg]
plusR_plus [in LogicProg]
plusS [in LogicProg]
plus_plusR [in LogicProg]
plus_ge [in DataStruct]
plus_n_Sm' [in MoreDep]
plus_assoc [in InductiveTypes]
plus_0 [in LogicProg]
plus_S [in InductiveTypes]
plus1 [in Universes]
predicate_extensionality [in Universes]
pred_strong1_irrel [in Universes]
pred_strong1_irrel' [in Universes]
present_insert_Black [in MoreDep]
present_balance1 [in MoreDep]
present_insert_Red [in MoreDep]
present_balance2 [in MoreDep]
present_ins [in MoreDep]
proj1 [in Universes]
proj1_again'' [in Universes]
proj1_again' [in Universes]
proj1_again [in Universes]
propify_holds [in Predicates]
propify_holds' [in Predicates]
propositional [in Match]

R

reassoc_correct [in Large]
reassoc_correct [in Large]
reassoc_correct [in Large]
reduce_me [in Equality]
rewr [in Large]
right_identity [in GeneralRec]
run_Bind [in GeneralRec]
run_Return [in GeneralRec]
run_Bottom [in GeneralRec]
run_Fix [in GeneralRec]

S

T

tassociativity [in GeneralRec]
tautTrue [in Reflection]
TBind_Answer [in GeneralRec]
tcompile_correct' [in StackMachine]
tcompile_correct [in StackMachine]
tcompile_correct' [in StackMachine]
tcompile_correct [in StackMachine]
tconcat_correct [in StackMachine]
test [in Match]
test_inster2 [in Match]
test_looper [in GeneralRec]
test_map [in GeneralRec]
test_mergeSort' [in GeneralRec]
test_inster [in Match]
test_mergeSort'' [in GeneralRec]
test1 [in Match]
test1 [in Match]
test2 [in Match]
test2 [in Match]
test2 [in Match]
test3 [in Match]
test3 [in Match]
test4 [in Match]
the_sky_is_falling [in InductiveTypes]
thunk_eq_refl [in GeneralRec]
thunk_eq_coind [in GeneralRec]
thunk_eq_frob [in GeneralRec]
times_1 [in LogicProg]
tleft_identity [in GeneralRec]
tright_identity [in GeneralRec]
true_galore [in Reflection]
true_galore' [in Reflection]
true_neq_false [in InductiveTypes]
True_conc [in Match]
twoEls_nil [in Predicates]
twoEls_two [in Predicates]
two_gt0 [in Subset]
t1 [in Reflection]
t1 [in Match]
t1 [in Universes]
t1' [in Match]
t2 [in Universes]
t2 [in Match]
t2' [in Universes]
t3 [in Universes]
t3 [in Match]
t3 [in Universes]
t4 [in Universes]
t4 [in Match]
t5 [in Match]
t5' [in Match]
t6 [in Match]
t6 [in Match]
t7 [in Match]
t8 [in Match]
t9 [in Match]

U

uhoh [in Universes]
uhoh_again [in Universes]
UIP [in Universes]
UIP_refl'' [in Equality]
UIP_refl [in Universes]
unique_ident [in Large]
unit_singleton [in InductiveTypes]

Z

zero_times [in LogicProg]
zgtz [in Universes]
zgtz [in Subset]

Section Index

A

All [in InductiveTypes]
autorewrite [in LogicProg]
autorewrite.garden_path [in LogicProg]
autorewrite.garden_path [in LogicProg]
autorewrite.garden_path [in LogicProg]

B

Bind [in GeneralRec]
Bottom [in GeneralRec]

C

cfoldCond [in DataStruct]
computation [in GeneralRec]
cond [in DataStruct]

D

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

E

evalCmd_coind [in Coinductive]
even_list_mut' [in InductiveTypes]

F

fhapp [in Equality]
fhapp' [in Equality]
fhlist [in Equality]
fhlist [in DataStruct]
fhlist_map [in Equality]
filist [in DataStruct]
firstorder [in Match]
firstorder' [in Match]
Fix [in GeneralRec]
forall_and [in LogicProg]
formula_ind' [in InductiveTypes]

H

hlist [in DataStruct]

I

ifoldr [in DataStruct]
ilist [in MoreDep]
ilist [in DataStruct]
ilist_map [in DataStruct]
insert [in MoreDep]
insert.present [in MoreDep]
interleave [in Coinductive]
In_dec [in Subset]

L

lattice [in GeneralRec]
list [in InductiveTypes]

M

map [in InductiveTypes]
map [in Coinductive]
map' [in Coinductive]
mergeSort [in GeneralRec]
monoid [in Reflection]
my_tauto [in Reflection]

N

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

O

ok [in Generic]

P

present [in MoreDep]
Propositional [in Predicates]
propositional [in Match]

R

Return [in GeneralRec]
rifoldr [in DataStruct]

S

slow [in LogicProg]
slow [in Large]
split [in MoreDep]
star [in MoreDep]
stream [in Coinductive]
stream_eq [in Coinductive]
stream_eq_loop [in Coinductive]
stream_eq_onequant [in Coinductive]
stream_eq_coind [in Coinductive]

T

test_inster [in Match]
thunk_eq_coind [in GeneralRec]
tree [in DataStruct]
tree [in Generic]
tree [in DataStruct]
twoEls [in Predicates]
t6 [in Match]
t7 [in Match]
t7 [in Match]

Constructor Index

A

Abs [in DataStruct]
And [in MoreDep]
And [in InductiveTypes]
And [in Subset]
And [in Universes]
And [in Reflection]
And [in Predicates]
And' [in Predicates]
And' [in Reflection]
Answer [in GeneralRec]
App [in DataStruct]
Arrow [in DataStruct]
Assign [in Coinductive]
Atomic [in Reflection]
Atomic' [in Reflection]

B

Bar [in Universes]
Base [in Universes]
BConst [in MoreDep]
BConst [in DataStruct]
Binop [in StackMachine]
Black [in MoreDep]
BlackNode [in MoreDep]
Bnd [in GeneralRec]
Bool [in Subset]
Bool [in StackMachine]
Bool [in MoreDep]
Bool [in DataStruct]

C

ChainCons [in GeneralRec]
Char [in MoreDep]
Con [in Generic]
Concat [in MoreDep]
Cond [in DataStruct]
conj [in Predicates]
Conjunction [in InductiveTypes]
Cons [in InductiveTypes]
Cons [in InductiveTypes]
Cons [in DataStruct]
Cons [in Coinductive]
Cons [in MoreDep]
Const [in LogicProg]
Const [in Universes]
Const [in DataStruct]
Const [in Coinductive]
Const [in Large]
Const [in Large]
Const [in StackMachine]
ConstP [in Universes]

E

ECons [in InductiveTypes]
Empty [in MoreDep]
ENil [in InductiveTypes]
Eq [in DataStruct]
Eq [in MoreDep]
Eq [in InductiveTypes]
Eq [in Universes]
EqAnswer [in GeneralRec]
EqP [in Universes]
EqThinkL [in GeneralRec]
EqThinkR [in GeneralRec]
EvalAnswer [in GeneralRec]
EvalAssign [in Coinductive]
EvalConst [in LogicProg]
EvalPlus [in LogicProg]
EvalSeq [in Coinductive]
EvalThink [in GeneralRec]
EvalVar [in LogicProg]
EvalWhileFalse [in Coinductive]
EvalWhileTrue [in Coinductive]
EvenO [in Predicates]
EvenSS [in Predicates]
Even_SS [in Reflection]
Even_O [in Reflection]
ExecBnd [in GeneralRec]
ExecRet [in GeneralRec]
ex_intro [in Predicates]

F

Fals [in Predicates]
false [in Predicates]
false [in InductiveTypes]
Falsehood [in Reflection]
Falsehood [in InductiveTypes]
Falsehood' [in Reflection]
FFAnd [in Predicates]
FFNot [in Predicates]
FFTru [in Predicates]
First [in DataStruct]
Foo [in Universes]
Forall [in Universes]
Forall [in InductiveTypes]
Found [in Subset]
Fst [in MoreDep]
Func [in Universes]

H

HAnd [in Predicates]
HAnd' [in Predicates]
HOr1 [in Predicates]
HOr1' [in Predicates]
HOr2 [in Predicates]
HOr2' [in Predicates]
HtAnd [in Subset]
HtBool [in Subset]
HtNat [in Subset]
HtPlus [in Subset]
HTru [in Predicates]
HTru' [in Predicates]

I

iBinop [in StackMachine]
iConst [in StackMachine]
Ident [in Reflection]
If [in MoreDep]
Imp [in Reflection]
Imp' [in Reflection]
Inject [in Universes]
IsZero [in Predicates]
Iter [in MoreDep]

L

Leaf [in DataStruct]
Leaf [in Generic]
Leaf [in MoreDep]
Leaf [in DataStruct]
Lift [in Universes]

M

MCons [in DataStruct]
MFirst [in DataStruct]
MNext [in DataStruct]
MNil [in DataStruct]
Mult [in Large]

N

Nat [in DataStruct]
Nat [in Subset]
Nat [in StackMachine]
Nat [in MoreDep]
NCons [in InductiveTypes]
NConst [in DataStruct]
NConst [in MoreDep]
Next [in DataStruct]
Nil [in DataStruct]
Nil [in MoreDep]
Nil [in InductiveTypes]
Nil [in InductiveTypes]
NLeaf [in InductiveTypes]
NLeaf' [in InductiveTypes]
NNil [in InductiveTypes]
NNode [in InductiveTypes]
NNode' [in InductiveTypes]
Node [in DataStruct]
Node [in DataStruct]
Node [in Generic]

O

O [in InductiveTypes]
OCons [in InductiveTypes]
Op [in Reflection]
Or [in Reflection]
Or [in Predicates]
Or [in MoreDep]
or_intror [in Predicates]
or_introl [in Predicates]
Or' [in Predicates]
Or' [in Reflection]

P

Pair [in Universes]
Pair [in MoreDep]
PairP [in Universes]
pair' [in Universes]
PAnd [in Universes]
PI [in Generic]
PInject [in Universes]
Plus [in MoreDep]
Plus [in Coinductive]
Plus [in LogicProg]
Plus [in Large]
Plus [in Large]
Plus [in Subset]
Plus [in DataStruct]
Plus [in StackMachine]
PlusO [in LogicProg]
PlusS [in LogicProg]
Prod [in MoreDep]

R

Red [in MoreDep]
RedNode [in MoreDep]
RedNode' [in MoreDep]
refl_equal [in Predicates]
Ret [in GeneralRec]

S

S [in InductiveTypes]
Seq [in Coinductive]
Snd [in MoreDep]
Star [in MoreDep]
Stream_eq [in Coinductive]

T

U

Unit [in DataStruct]
Unknown [in Subset]

V

Var [in Coinductive]
Var [in Reflection]
Var [in DataStruct]
Var [in LogicProg]
VarEq [in Universes]

W

While [in Coinductive]

Notation Index

M

_ + _ [in Reflection]

other

_ --> _ [in Reflection]
_ --> _ [in Match]
_ ;;; _ [in Subset]
_ * _ [in LogicProg]
_ ;; _ [in Subset]
_ <- _ ; _ [in GeneralRec]
_ <- _ ; _ [in GeneralRec]
_ === _ [in Equality]
_ <- _ ; _ [in Subset]
_ <- _ ; _ [in GeneralRec]
_ || _ [in Subset]
_ == _ [in Equality]
_ <-- _ ; _ [in Subset]
No [in Subset]
Reduce _ [in Subset]
Yes [in Subset]
!! [in Subset]
! [in Subset]
?? [in Subset]
[ ! , _ ~> _ ] [in Generic]
[ ! , ! ~> _ ] [in Generic]
[ _ , _ ~> _ ] [in Generic]
[ _ ] [in Subset]
[ _ , ! ~> _ ] [in Generic]
[| _ |] [in Subset]
[|| _ ||] [in Subset]
^ [in Generic]
{< _ >} [in MoreDep]
{{ _ | _ }} [in Subset]

Inductive Index

A

and [in Predicates]

B

bar [in Universes]
binop [in StackMachine]
bool [in Predicates]
bool [in InductiveTypes]

C

cmd [in Coinductive]
color [in MoreDep]
comp [in GeneralRec]

E

Empty_set [in Predicates]
Empty_set [in InductiveTypes]
eq [in Predicates]
eqPlus [in Universes]
eval [in GeneralRec]
eval [in LogicProg]
evalCmd [in Coinductive]
even [in Predicates]
even_list [in InductiveTypes]
ex [in Predicates]
exec [in GeneralRec]
exp [in Subset]
exp [in StackMachine]
exp [in Coinductive]
exp [in Universes]
exp [in Large]
exp [in DataStruct]
exp [in LogicProg]
exp [in MoreDep]
exp [in Large]
expP [in Universes]
exp' [in DataStruct]

F

falseFree [in Predicates]
fin [in DataStruct]
foo [in Universes]
formula [in InductiveTypes]
formula [in Reflection]
formula [in Universes]
formula' [in Reflection]

H

hasType [in Subset]
hlist [in DataStruct]
holds [in Predicates]
holds' [in Predicates]

I

ilist [in MoreDep]
ilist [in DataStruct]
instr [in StackMachine]
isChain [in GeneralRec]
isEven [in Reflection]
isZero [in Predicates]

L

list [in InductiveTypes]
list [in InductiveTypes]

M

maybe [in Subset]
member [in DataStruct]
mexp [in Reflection]

N

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

O

odd_list [in InductiveTypes]
or [in Predicates]

P

pformula [in InductiveTypes]
plusR [in LogicProg]
prod [in Predicates]
prod' [in Universes]
proof [in Universes]
prop [in Predicates]
prop' [in Predicates]

R

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

S

star [in MoreDep]
stream [in Coinductive]
stream_eq [in Coinductive]
sum [in Predicates]

T

taut [in Reflection]
tbinop [in StackMachine]
texp [in StackMachine]
thunk [in GeneralRec]
thunk_eq [in GeneralRec]
tinstr [in StackMachine]
tprog [in StackMachine]
tree [in Generic]
tree [in DataStruct]
tree [in DataStruct]
twoEls [in Predicates]
type [in DataStruct]
type [in MoreDep]
type [in Subset]
type [in StackMachine]
type' [in DataStruct]

U

unit [in Predicates]
unit [in InductiveTypes]

Definition Index

A

add [in Reflection]
addLists [in Equality]
addLists' [in Equality]
All [in InductiveTypes]
allTrue [in Reflection]
always_O' [in InductiveTypes]
always_O [in InductiveTypes]
app [in InductiveTypes]
app [in InductiveTypes]
app [in MoreDep]
approx [in Coinductive]
app' [in MoreDep]
asgn [in Reflection]
a_b [in MoreDep]
a_star [in MoreDep]

B

backward [in Reflection]
balance1 [in MoreDep]
balance2 [in MoreDep]
Bind [in GeneralRec]
binopDenote [in StackMachine]
bool_fix [in Generic]
bool_den [in Generic]
bool_dt [in Generic]
Bottom [in GeneralRec]

C

cast [in Universes]
cfold [in MoreDep]
cfold [in DataStruct]
cfoldCond [in DataStruct]
check_even [in Reflection]
choice_Set [in Universes]
compile [in StackMachine]
computation [in GeneralRec]
comp_eq [in GeneralRec]
cond [in DataStruct]
constructorDenote [in Generic]
curriedAdd [in GeneralRec]
curriedAdd' [in GeneralRec]

D

datatype [in Generic]
datatypeDenote [in Generic]
datatypeDenoteOk [in Generic]
dec_star'' [in MoreDep]
dec_star [in MoreDep]
dec_star' [in MoreDep]
depth [in MoreDep]
doublePred [in Subset]
doublePred' [in Subset]

E

eapp [in InductiveTypes]
elength [in InductiveTypes]
Empty_set_dt [in Generic]
Empty_set_fix [in Generic]
Empty_set_den [in Generic]
eq_type_dec [in Subset]
eq_nat_dec [in Subset]
eq_nat_dec' [in Subset]
eval [in Large]
eval [in Large]
evalExp [in Coinductive]
eval1 [in LogicProg]
eval1' [in LogicProg]
eval1' [in LogicProg]
even_list_mut' [in InductiveTypes]
expDenote [in MoreDep]
expDenote [in DataStruct]
expDenote [in StackMachine]
exp'Denote [in DataStruct]
ex1 [in DataStruct]
e2u [in InductiveTypes]

F

fact [in GeneralRec]
fact_slow [in Coinductive]
fact_iter' [in Coinductive]
fact_iter [in Coinductive]
fact_slow' [in Coinductive]
falses_trues [in Coinductive]
ffin [in DataStruct]
fget [in DataStruct]
fhapp [in Equality]
fhget [in Equality]
fhget [in DataStruct]
fhlist [in DataStruct]
fhlist [in Equality]
fhmap [in Equality]
filist [in DataStruct]
finOut [in Universes]
five_plus_three' [in LogicProg]
Fix [in GeneralRec]
fixDenote [in Generic]
fixDenoteOk [in Generic]
Fix' [in GeneralRec]
flatten [in Reflection]
fmember [in Equality]
fmember [in DataStruct]
forall_refl [in InductiveTypes]
formulaDenote [in InductiveTypes]
formulaDenote [in Reflection]
formula_ind' [in InductiveTypes]
forward [in Reflection]
four_plus_three [in LogicProg]
four_plus_three' [in LogicProg]
frob [in Coinductive]
frob [in GeneralRec]
frob' [in GeneralRec]

G

get [in DataStruct]

H

hd [in MoreDep]
hd [in Coinductive]
hd' [in MoreDep]
hget [in DataStruct]
hi [in MoreDep]
holds [in Reflection]
hundred_minus_hundred [in LogicProg]

I

id [in Universes]
id [in Universes]
id [in Equality]
id' [in Equality]
ifoldr [in DataStruct]
imap [in DataStruct]
imp [in Match]
imp [in Reflection]
inc [in DataStruct]
inc [in DataStruct]
index_eq [in Reflection]
inject [in MoreDep]
ins [in MoreDep]
insert [in GeneralRec]
insert [in MoreDep]
insertResult [in MoreDep]
insResult [in MoreDep]
instrDenote [in StackMachine]
interleave [in Coinductive]
Int.e [in Large]
Int.f [in Large]
Int.G [in Large]
Int.i [in Large]
In_dec [in Subset]
In_dec [in Reflection]
isZero [in InductiveTypes]

J

JMeq' [in Equality]

L

lemma1' [in Equality]
lemma2 [in Equality]
length [in InductiveTypes]
length [in InductiveTypes]
lengthOrder [in GeneralRec]
length_1_2 [in LogicProg]
length_and_sum'' [in LogicProg]
length_and_sum' [in LogicProg]
length_is_2 [in LogicProg]
length_is_2 [in LogicProg]
length_and_sum [in LogicProg]
leq [in GeneralRec]
list_fix [in Generic]
list_dt [in Generic]
list_den [in Generic]
looper [in GeneralRec]

M

makeRbtree [in MoreDep]
map [in GeneralRec]
map [in Coinductive]
map [in InductiveTypes]
map [in Generic]
map_nat [in Generic]
matches [in MoreDep]
mdenote [in Reflection]
meq [in GeneralRec]
merge [in GeneralRec]
mergeSort [in GeneralRec]
mergeSort' [in GeneralRec]
mergeSort'' [in GeneralRec]
mldenote [in Reflection]
my_tauto [in Reflection]

N

napp [in InductiveTypes]
nat_dt [in Generic]
nat_fix [in Generic]
nat_den [in Generic]
nat_tree_ind' [in InductiveTypes]
nat_ind' [in InductiveTypes]
needs_trans [in LogicProg]
negb [in InductiveTypes]
negb' [in InductiveTypes]
nlength [in InductiveTypes]
nsize [in InductiveTypes]
nsplice [in InductiveTypes]
ntsize [in InductiveTypes]
ntsplice [in InductiveTypes]

O

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

P

R

reassoc [in Large]
Return [in GeneralRec]
rifoldr [in DataStruct]
rpresent [in MoreDep]
run [in GeneralRec]
runTo [in GeneralRec]

S

set [in Coinductive]
seven_minus_three_again [in LogicProg]
seven_minus_four [in LogicProg]
seven_minus_three [in LogicProg]
seven_minus_three [in LogicProg]
seven_minus_four_zero [in LogicProg]
seven_minus_three' [in LogicProg]
seven_minus_four' [in LogicProg]
size [in Generic]
somePairs [in DataStruct]
someTypes [in DataStruct]
someValues [in DataStruct]
split [in MoreDep]
split' [in MoreDep]
stack [in StackMachine]
sum [in DataStruct]
sum [in DataStruct]
sum [in LogicProg]
sum [in InductiveTypes]
swapper [in InductiveTypes]
sym_ex [in Universes]
sym_sig [in Universes]
synthesize1 [in LogicProg]
synthesize2 [in LogicProg]
synthesize3 [in LogicProg]

T

tautDenote [in Reflection]
TBind [in GeneralRec]
tbinopDenote [in StackMachine]
tcompile [in StackMachine]
tconcat [in StackMachine]
testCurriedAdd [in GeneralRec]
texpDenote [in StackMachine]
three_minus_four_zero [in LogicProg]
three_minus_four_zero [in LogicProg]
times [in Large]
times [in Large]
times [in Large]
times [in Large]
tinstrDenote [in StackMachine]
tl [in Coinductive]
toProp [in InductiveTypes]
tprogDenote [in StackMachine]
tree_den [in Generic]
tree_dt [in Generic]
tree_fix [in Generic]
trues_falses [in Coinductive]
tstack [in StackMachine]
typeCheck [in Subset]
typeCheck' [in Subset]
typeDenote [in DataStruct]
typeDenote [in StackMachine]
typeDenote [in MoreDep]
type'Denote [in DataStruct]

U

UIP_refl' [in Equality]
unit_den [in Generic]
unit_fix [in Generic]
unit_dt [in Generic]
unit_rect' [in InductiveTypes]
unject [in MoreDep]

V

var [in Coinductive]
vars [in Coinductive]
vstack [in StackMachine]

Z

zeroes [in Coinductive]

Module Index

G

Group [in Large]
GROUP [in Large]
GROUP_THEOREMS.M [in Large]
GROUP_THEOREMS [in Large]
Group.M [in Large]

I

Int [in Large]
IntTheorems [in Large]

Axiom Index

C

classic [in Universes]

E

ext_eq [in Equality]

G

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

N

n [in Universes]
not_classic [in Universes]

P

positive [in Universes]

Variable Index

A

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

B

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

C

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

D

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

E

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

F

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

G

G [in LogicProg]

H

hlist.A [in DataStruct]
hlist.B [in DataStruct]
hlist.elm [in DataStruct]

I

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

L

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

M

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

N

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

O

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

P

present.x [in MoreDep]
Propositional.P [in Predicates]
propositional.P [in Match]
propositional.Q [in Match]
Propositional.Q [in Predicates]
propositional.R [in Match]
Propositional.R [in Predicates]

R

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

S

T

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

Library Index

C

Coinductive

D

DataStruct

E

Equality

G

GeneralRec
Generic

I

InductiveTypes
Intro

L

Large
LogicProg

M

Match
MoreDep

P

Predicates

R

Reflection

S

StackMachine
Subset

U

Universes

Global Index

other

(1280 entries)

Projection Index

other

(4 entries)

Record Index

other

(2 entries)

Lemma Index

other

(328 entries)

Section Index

other

(70 entries)

Constructor Index

other

(217 entries)

Notation Index

other

(30 entries)

Inductive Index

other

(90 entries)

Definition Index

other

(286 entries)

Module Index

other

(7 entries)

Axiom Index

other

(15 entries)

Variable Index

other

(215 entries)

Library Index

other

(16 entries)

This page has been generated by coqdoc