Global Index

(1612 entries)

Projection Index

(4 entries)

Record Index

(2 entries)

Lemma Index

(369 entries)

Section Index

(87 entries)

Constructor Index

(382 entries)

Inductive Index

(128 entries)

Definition Index

(363 entries)

Module Index

(18 entries)

Axiom Index

(18 entries)

Variable Index

(220 entries)

Library Index

(21 entries)

Global Index

A

Abs [definition, in Hoas]
Abs [constructor, in OpSem]
Abs [constructor, in DataStruct]
Abs [constructor, in DeBruijn]
Abs' [constructor, in Hoas]
add [definition, in Reflection]
add_self [definition, in Hoas]
All [section, in InductiveTypes]
All [definition, in InductiveTypes]
allTrue [definition, in Reflection]
allTrue_add [lemma, in Reflection]
allTrue_In [lemma, in Reflection]
All.P [variable, in InductiveTypes]
All.T [variable, in InductiveTypes]
always_O [definition, in InductiveTypes]
always_O' [definition, in InductiveTypes]
always_safe [lemma, in Coinductive]
And [constructor, in Reflection]
And [constructor, in MoreDep]
And [constructor, in InductiveTypes]
And [constructor, in Predicates]
And [constructor, in Hoas]
And [constructor, in Subset]
And' [constructor, in Predicates]
and_assoc [lemma, in Predicates]
and_comm [lemma, in Predicates]
and_True_conc [lemma, in Match]
and_True_prem [lemma, in Match]
app [definition, in InductiveTypes]
app [definition, in InductiveTypes]
App [constructor, in DataStruct]
app [definition, in Hoas]
App [constructor, in DeBruijn]
app [definition, in MoreDep]
App [constructor, in OpSem]
App [definition, in Hoas]
AppCong1 [constructor, in Hoas]
AppCong2 [constructor, in Hoas]
append_emp [lemma, in MoreDep]
approx [definition, in Coinductive]
App' [constructor, in Hoas]
app' [definition, in MoreDep]
app_cong [lemma, in MoreDep]
app_empty_end [lemma, in MoreDep]
app_ident [definition, in Hoas]
app_ident' [definition, in Hoas]
app_ident1 [definition, in Hoas]
app_zero [definition, in Hoas]
arith_comm [lemma, in Predicates]
arith_comm' [lemma, in Predicates]
arith_neq [lemma, in Predicates]
arith_neq' [lemma, in Predicates]
Arrow [constructor, in DataStruct]
Arrow [constructor, in Hoas]
Arrow [constructor, in Intensional]
asgn [definition, in Reflection]
assoc_conc1 [lemma, in Match]
assoc_conc2 [lemma, in Match]
assoc_prem1 [lemma, in Match]
assoc_prem2 [lemma, in Match]
Atomic [constructor, in Reflection]
autorewrite [section, in Match]
autorewrite.A [variable, in Match]
autorewrite.f [variable, in Match]
autorewrite.f_f [variable, in Match]
autorewrite.garden_path [section, in Match]
autorewrite.garden_path [section, in Match]
autorewrite.garden_path [section, in Match]
autorewrite.garden_path.f_g [variable, in Match]
autorewrite.garden_path.f_g [variable, in Match]
autorewrite.garden_path.f_g [variable, in Match]
autorewrite.garden_path.g [variable, in Match]
autorewrite.garden_path.g [variable, in Match]
autorewrite.garden_path.g [variable, in Match]
autorewrite.garden_path.P [variable, in Match]
autorewrite.garden_path.P [variable, in Match]
a_b [definition, in MoreDep]
a_star [definition, in MoreDep]

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 DataStruct]
BConst [constructor, in MoreDep]
Beta [constructor, in Hoas]
BigStep [inductive, in Hoas]
Big_Multi [lemma, in Hoas]
Big_Val [lemma, in Hoas]
Big_Val' [lemma, in Hoas]
binop [inductive, in StackMachine]
Binop [constructor, in StackMachine]
binopDenote [definition, in StackMachine]
Black [constructor, in MoreDep]
BlackNode [constructor, in MoreDep]
Bool [constructor, in Subset]
Bool [constructor, in MoreDep]
bool [inductive, in InductiveTypes]
Bool [constructor, in DataStruct]
Bool [constructor, in StackMachine]
bool_den [definition, in Generic]
bool_dt [definition, in Generic]
bool_fix [definition, in Generic]
bool_neq [lemma, in Match]
bool_neq [lemma, in Match]

C

CAbs [constructor, in Hoas]
CApp [constructor, in Hoas]
cast [definition, in Universes]
CConst [constructor, in Hoas]
cfold [definition, in DataStruct]
cfold [definition, in MoreDep]
cfoldCond [definition, in DataStruct]
cfoldCond [section, in DataStruct]
cfoldCond.default [variable, in DataStruct]
cfoldCond.t [variable, in DataStruct]
cfoldCond_correct [lemma, in DataStruct]
cfold_correct [lemma, in DataStruct]
cfold_correct [lemma, in Large]
cfold_correct [lemma, in Large]
cfold_correct [lemma, in MoreDep]
cfold_correct [lemma, in Large]
Char [constructor, in MoreDep]
check_even [definition, in Reflection]
choice_Set [definition, in Universes]
classic [axiom, in Universes]
classic_nat_eq [lemma, in Universes]
closed [axiom, in Hoas]
Closed [inductive, in Hoas]
Coinductive [library]
color [inductive, in MoreDep]
comm_conc [lemma, in Match]
comm_prem [lemma, in Match]
compile [definition, in StackMachine]
compile_correct [lemma, in StackMachine]
compile_correct [lemma, in StackMachine]
compile_correct' [lemma, in StackMachine]
compile_correct' [lemma, in StackMachine]
Con [constructor, in Generic]
Concat [constructor, in MoreDep]
Concrete [module, in Firstorder]
Concrete.Abs [constructor, in Firstorder]
Concrete.App [constructor, in Firstorder]
Concrete.Arrow [constructor, in Firstorder]
Concrete.Beta [constructor, in Firstorder]
Concrete.Bool [constructor, in Firstorder]
Concrete.Cong1 [constructor, in Firstorder]
Concrete.Cong2 [constructor, in Firstorder]
Concrete.Const [constructor, in Firstorder]
Concrete.ctx [definition, in Firstorder]
Concrete.disjoint_cons [lemma, in Firstorder]
Concrete.exp [inductive, in Firstorder]
Concrete.First [constructor, in Firstorder]
Concrete.hasType [inductive, in Firstorder]
Concrete.lookup [inductive, in Firstorder]
Concrete.Next [constructor, in Firstorder]
Concrete.preservation [lemma, in Firstorder]
Concrete.preservation' [lemma, in Firstorder]
Concrete.progress [lemma, in Firstorder]
Concrete.progress' [lemma, in Firstorder]
Concrete.shadow_hasType [lemma, in Firstorder]
Concrete.shadow_hasType' [lemma, in Firstorder]
Concrete.shadow_lookup [lemma, in Firstorder]
Concrete.step [inductive, in Firstorder]
Concrete.subst [section, in Firstorder]
Concrete.subst [definition, in Firstorder]
Concrete.subst.e1 [variable, in Firstorder]
Concrete.subst.Ht' [variable, in Firstorder]
Concrete.subst.x [variable, in Firstorder]
Concrete.subst.xt [variable, in Firstorder]
Concrete.subst_hasType [lemma, in Firstorder]
Concrete.subst_hasType_closed [lemma, in Firstorder]
Concrete.subst_lookup [lemma, in Firstorder]
Concrete.subst_lookup' [lemma, in Firstorder]
Concrete.TAbs [constructor, in Firstorder]
Concrete.TApp [constructor, in Firstorder]
Concrete.TConst [constructor, in Firstorder]
Concrete.TVar [constructor, in Firstorder]
Concrete.type [inductive, in Firstorder]
Concrete.VAbs [constructor, in Firstorder]
Concrete.val [inductive, in Firstorder]
Concrete.Var [constructor, in Firstorder]
Concrete.var [definition, in Firstorder]
Concrete.var_eq [definition, in Firstorder]
Concrete.VConst [constructor, in Firstorder]
Concrete.weaken_hasType [lemma, in Firstorder]
Concrete.weaken_hasType' [lemma, in Firstorder]
Concrete.weaken_lookup [lemma, in Firstorder]
cond [definition, in DataStruct]
cond [section, in DataStruct]
Cond [constructor, in DataStruct]
cond.A [variable, in DataStruct]
cond.default [variable, in DataStruct]
cond_ext [lemma, in DataStruct]
confounder [lemma, in Large]
Cong [constructor, in Hoas]
Cons [constructor, in InductiveTypes]
Cons [constructor, in Coinductive]
Cons [constructor, in MoreDep]
Cons [constructor, in DataStruct]
Cons [constructor, in InductiveTypes]
Const [constructor, in Large]
Const [definition, in Hoas]
Const [constructor, in DataStruct]
Const [constructor, in StackMachine]
Const [constructor, in Universes]
Const [constructor, in Large]
ConstP [constructor, in Universes]
constructor [record, in Generic]
constructorDenote [definition, in Generic]
Const' [constructor, in Hoas]
contra [lemma, in Predicates]
Copy [constructor, in Coinductive]
countOne [definition, in Hoas]
CountOne [definition, in Hoas]
CountVars [definition, in Hoas]
countVars [definition, in Hoas]
CPlus [constructor, in Hoas]
CPS [module, in Extensional]
CPS [module, in OpSem]
CpsExp [definition, in Extensional]
cpsExp [definition, in Extensional]
CpsExp [definition, in OpSem]
cpsExp [definition, in OpSem]
cpsExp [section, in Extensional]
cpsExp [section, in OpSem]
cpsExp.var [variable, in OpSem]
cpsExp.var [variable, in Extensional]
CpsExp_correct [lemma, in OpSem]
cpsExp_correct [lemma, in OpSem]
CpsExp_correct [lemma, in Extensional]
cpsExp_correct [lemma, in Extensional]
cpsFunc [definition, in OpSem]
cpsType [definition, in Extensional]
CPS.Abs [constructor, in OpSem]
CPS.Abs [constructor, in Extensional]
CPS.App [constructor, in OpSem]
CPS.App [constructor, in Extensional]
CPS.Bind [constructor, in OpSem]
CPS.Bind [constructor, in Extensional]
CPS.Bool [constructor, in OpSem]
CPS.closure [definition, in OpSem]
CPS.closures [definition, in OpSem]
CPS.Const [constructor, in Extensional]
CPS.Cont [constructor, in Extensional]
CPS.EvAbs [constructor, in OpSem]
CPS.Eval [definition, in OpSem]
CPS.eval [inductive, in OpSem]
CPS.evalP [inductive, in OpSem]
CPS.EvApp [constructor, in OpSem]
CPS.EvBind [constructor, in OpSem]
CPS.EvBool [constructor, in OpSem]
CPS.EvFst [constructor, in OpSem]
CPS.EvHalt [constructor, in OpSem]
CPS.EvPair [constructor, in OpSem]
CPS.EvSnd [constructor, in OpSem]
CPS.exp [section, in OpSem]
CPS.exp.var [variable, in OpSem]
CPS.Fst [constructor, in OpSem]
CPS.Fst [constructor, in Extensional]
CPS.Halt [constructor, in OpSem]
CPS.Pair [constructor, in OpSem]
CPS.Pair [constructor, in Extensional]
CPS.PHalt [constructor, in Extensional]
CPS.Plus [constructor, in Extensional]
CPS.Primop [definition, in OpSem]
CPS.Primop [definition, in Extensional]
CPS.primop [inductive, in Extensional]
CPS.primop [inductive, in OpSem]
CPS.PrimopDenote [definition, in Extensional]
CPS.primopDenote [definition, in Extensional]
CPS.Prod [constructor, in Extensional]
CPS.prog [inductive, in OpSem]
CPS.prog [inductive, in Extensional]
CPS.Prog [definition, in OpSem]
CPS.Prog [definition, in Extensional]
CPS.progDenote [definition, in Extensional]
CPS.ProgDenote [definition, in Extensional]
CPS.Snd [constructor, in Extensional]
CPS.Snd [constructor, in OpSem]
CPS.TNat [constructor, in Extensional]
CPS.type [inductive, in Extensional]
CPS.typeDenote [definition, in Extensional]
CPS.val [inductive, in OpSem]
CPS.vars [section, in Extensional]
CPS.vars.var [variable, in Extensional]
CPS.VBool [constructor, in OpSem]
CPS.VFun [constructor, in OpSem]
CPS.VPair [constructor, in OpSem]
cr [section, in OpSem]
cr [inductive, in OpSem]
CrBool [constructor, in OpSem]
CrFun [constructor, in OpSem]
cr.s1 [variable, in OpSem]
cr.s2 [variable, in OpSem]
cr_monotone [lemma, in OpSem]
Ctx [inductive, in Hoas]

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 InductiveTypes]
Empty_set_den [definition, in Generic]
Empty_set_dt [definition, in Generic]
Empty_set_fix [definition, in Generic]
ENil [constructor, in InductiveTypes]
Eq [constructor, in Universes]
Eq [constructor, in Hoas]
Eq [constructor, in MoreDep]
Eq [constructor, in DataStruct]
Eq [constructor, in InductiveTypes]
EqP [constructor, in Universes]
eqPlus [inductive, in Universes]
Equality [library]
eq_bool [definition, in StackMachine]
eq_nat [definition, in StackMachine]
eq_nat_dec [definition, in Subset]
eq_nat_dec' [definition, in Subset]
eq_type_dec [definition, in Subset]
eval [definition, in Large]
eval [definition, in Large]
eval_double [lemma, in Large]
eval_monotone [lemma, in OpSem]
eval_times [lemma, in Large]
eval_times [lemma, in Large]
eval_times [lemma, in Large]
eval_times [lemma, in Large]
eval_times [lemma, in Large]
eval_times [lemma, in Large]
eval_times [lemma, in Large]
even [inductive, in Predicates]
EvenO [constructor, in Predicates]
EvenSS [constructor, in Predicates]
even_contra [lemma, in Predicates]
even_contra [lemma, in Predicates]
even_contra' [lemma, in Predicates]
even_contra'' [lemma, in Predicates]
even_list [inductive, in InductiveTypes]
even_list_mut' [definition, in InductiveTypes]
even_list_mut' [section, in InductiveTypes]
even_list_mut'.ECons_case [variable, in InductiveTypes]
even_list_mut'.ENil_case [variable, in InductiveTypes]
even_list_mut'.OCons_case [variable, in InductiveTypes]
even_list_mut'.Peven [variable, in InductiveTypes]
even_list_mut'.Podd [variable, in InductiveTypes]
Even_O [constructor, in Reflection]
even_plus [lemma, in Predicates]
Even_SS [constructor, in Reflection]
even_0 [lemma, in Predicates]
even_1_contra [lemma, in Predicates]
even_255 [lemma, in Reflection]
even_256 [lemma, in Reflection]
even_256' [lemma, in Reflection]
even_3_contra [lemma, in Predicates]
even_4 [lemma, in Predicates]
even_4' [lemma, in Predicates]
exec [inductive, in Coinductive]
exec_total [lemma, in Coinductive]
Exists [constructor, in Hoas]
exist1 [lemma, in Predicates]
exist2 [lemma, in Predicates]
exotic_prop [definition, in Hoas]
exp [inductive, in Hoas]
exp [inductive, in Large]
exp [inductive, in Subset]
Exp [definition, in Hoas]
exp [inductive, in MoreDep]
exp [inductive, in DeBruijn]
exp [inductive, in Large]
exp [inductive, in OpSem]
exp [section, in Hoas]
exp [inductive, in Universes]
exp [inductive, in DataStruct]
exp [inductive, in StackMachine]
exp [section, in OpSem]
expDenote [definition, in MoreDep]
expDenote [definition, in StackMachine]
expDenote [definition, in DataStruct]
expP [inductive, in Universes]
exp' [inductive, in DataStruct]
exp'Denote [definition, in DataStruct]
exp.var [variable, in Hoas]
exp.var [variable, in OpSem]
Exp1 [definition, in Hoas]
extends [definition, in OpSem]
extends1 [lemma, in OpSem]
extends_lookup [lemma, in OpSem]
extends_refl [lemma, in OpSem]
extends_trans [lemma, in OpSem]
Extensional [library]
ext_eq [axiom, in Equality]
ex_conc [lemma, in Match]
ex_prem [lemma, in Match]
e2u [definition, in InductiveTypes]
E_Copy [constructor, in Coinductive]
E_Imm [constructor, in Coinductive]
E_Jmp [constructor, in Coinductive]
E_JnzF [constructor, in Coinductive]
E_JnzT [constructor, in Coinductive]

F

f [definition, in InductiveTypes]
Fals [constructor, in Predicates]
false [constructor, in InductiveTypes]
falseFree [inductive, in Predicates]
falseFree_holds [lemma, in Predicates]
Falsehood [constructor, in Reflection]
falses [definition, in Coinductive]
False_imp [lemma, in Predicates]
False_prem [lemma, in Match]
false_prop [definition, in Hoas]
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' [section, in Equality]
fhapp'.A [variable, in Equality]
fhapp'.B [variable, in Equality]
fhapp.A [variable, in Equality]
fhapp.B [variable, in Equality]
fhapp_ass [lemma, in Equality]
fhapp_ass' [lemma, in Equality]
fhget [definition, in DataStruct]
fhget [definition, in Equality]
fhlist [section, in DataStruct]
fhlist [section, in Equality]
fhlist [definition, in DataStruct]
fhlist [definition, in Equality]
fhlist.A [variable, in DataStruct]
fhlist.A [variable, in Equality]
fhlist.B [variable, in DataStruct]
fhlist.B [variable, in Equality]
fhlist.elm [variable, in Equality]
fhlist.elm [variable, in DataStruct]
fhlist_map [section, in Equality]
fhlist_map.A [variable, in Equality]
fhlist_map.B [variable, in Equality]
fhlist_map.C [variable, in Equality]
fhlist_map.elm [variable, in Equality]
fhlist_map.f [variable, in Equality]
fhmap [definition, in Equality]
filist [section, in DataStruct]
filist [definition, in DataStruct]
filist.A [variable, in DataStruct]
fin [inductive, in DataStruct]
fin_ge [inductive, in DeBruijn]
fin_ge_inv [lemma, in DeBruijn]
fin_ge_inv' [lemma, in DeBruijn]
fin_inv [lemma, in DeBruijn]
First [constructor, in DataStruct]
firstorder [section, in Match]
Firstorder [library]
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]
fixDenote [definition, in Generic]
fixDenoteOk [definition, in Generic]
flatten [section, in Hoas]
flatten [definition, in Reflection]
flatten [definition, in Hoas]
flatten.var [variable, in Hoas]
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 InductiveTypes]
Forall [constructor, in Hoas]
forall_and [section, in Match]
forall_and [lemma, in Match]
forall_and.A [variable, in Match]
forall_and.both [variable, in Match]
forall_and.P [variable, in Match]
forall_and.Q [variable, in Match]
forall_eq [lemma, in Equality]
forall_exists_commute [lemma, in Predicates]
forall_refl [definition, in InductiveTypes]
formula [inductive, in Reflection]
formula [inductive, in InductiveTypes]
formulaDenote [definition, in InductiveTypes]
formulaDenote [definition, in Reflection]
formula_ind' [definition, in InductiveTypes]
formula_ind' [section, in InductiveTypes]
formula_ind'.And_case [variable, in InductiveTypes]
formula_ind'.Eq_case [variable, in InductiveTypes]
formula_ind'.Forall_case [variable, in InductiveTypes]
formula_ind'.P [variable, in InductiveTypes]
forward [definition, in Reflection]
Found [constructor, in Subset]
fo' [lemma, in Match]
frob [definition, in Coinductive]
frob_eq [lemma, in Coinductive]
Fst [constructor, in MoreDep]
Func [constructor, in Universes]
f_f_f [lemma, in Match]
f_f_f' [lemma, in Match]
f_f_f' [lemma, in Match]
f_f_f' [lemma, in Match]
f_f_f_g [lemma, in Match]

G

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 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]
Hoas [library]
holds [inductive, in Predicates]
holds [definition, in Reflection]
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]

I

IBinop [constructor, in StackMachine]
IConst [constructor, in StackMachine]
id [definition, in Universes]
id [definition, in Universes]
ident [definition, in Hoas]
Ident [constructor, in Reflection]
ident1 [definition, in Hoas]
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 DataStruct]
ilist [inductive, in DataStruct]
ilist [section, in MoreDep]
ilist [inductive, in MoreDep]
ilist.A [variable, in DataStruct]
ilist.A [variable, in MoreDep]
ilist_map [section, in DataStruct]
ilist_map.A [variable, in DataStruct]
ilist_map.B [variable, in DataStruct]
ilist_map.f [variable, in DataStruct]
imap [definition, in DataStruct]
Imm [constructor, in Coinductive]
imp [definition, in Reflection]
imp [definition, in Match]
Imp [constructor, in Reflection]
imp_True [lemma, in Match]
inc [definition, in DataStruct]
inc [definition, in DataStruct]
index_eq [definition, in Reflection]
InductiveTypes [library]
inject [definition, in MoreDep]
inject_inverse [lemma, in MoreDep]
ins [definition, in MoreDep]
insert [definition, in MoreDep]
insert [section, 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 Coinductive]
instr [inductive, in StackMachine]
instrDenote [definition, in StackMachine]
Int [module, in Large]
Intensional [library]
interleave [definition, in Coinductive]
interleave [section, in Coinductive]
interleave.A [variable, in Coinductive]
Interps [library]
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 Reflection]
In_dec [definition, in Subset]
In_dec [section, in Subset]
In_dec.A [variable, in Subset]
In_dec.A_eq_dec [variable, in Subset]
In_makeG' [lemma, in Intensional]
In_makeG'_contra [lemma, in Intensional]
In_makeG'_contra' [lemma, in Intensional]
in_star [lemma, in Match]
In_zip [lemma, in Intensional]
IsApp1 [constructor, in Hoas]
IsApp2 [constructor, in Hoas]
isCtx [inductive, in Hoas]
isEven [inductive, in Reflection]
IsPlus1 [constructor, in Hoas]
IsPlus2 [constructor, in Hoas]
isZero [inductive, in Predicates]
isZero [definition, in InductiveTypes]
IsZero [constructor, in Predicates]
isZero_contra [lemma, in Predicates]
isZero_contra' [lemma, in Predicates]
isZero_plus [lemma, in Predicates]
isZero_zero [lemma, in Predicates]
Iter [constructor, in MoreDep]

J

JMeq' [definition, in Equality]
JMeq_eq' [lemma, in Equality]
JMeq_refl' [lemma, in Equality]
Jmp [constructor, in Coinductive]
Jnz [constructor, in Coinductive]

L

M

M [module, in Large]
M [module, in Large]
makeG [definition, in Intensional]
makeG' [definition, in Intensional]
makeRbtree [definition, in MoreDep]
makeVar [definition, in Intensional]
map [definition, in Generic]
map [definition, in Coinductive]
map [definition, in InductiveTypes]
map [section, in InductiveTypes]
map [section, in Coinductive]
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]
map_id [lemma, in Generic]
map_nat [definition, in Generic]
Match [lemma, in Match]
Match [library]
matches [definition, in MoreDep]
maybe [inductive, in Subset]
MCons [constructor, in DataStruct]
mdenote [definition, in Reflection]
member [inductive, in DataStruct]
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.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]
monoid_reflect [lemma, in Reflection]
more [definition, in DeBruijn]
MoreDep [library]
mt1 [lemma, in Reflection]
mt2 [lemma, in Reflection]
mt3 [lemma, in Reflection]
mt4 [lemma, in Reflection]
mt4' [lemma, in Reflection]
Mult [constructor, in Large]
MultiStep [inductive, in Hoas]
MultiStep_trans [lemma, in Hoas]
Multi_Big [lemma, in Hoas]
Multi_Big' [lemma, in Hoas]
Multi_Cong [lemma, in Hoas]
Multi_Cong' [lemma, in Hoas]
my_tauto [definition, in Reflection]
my_tauto [section, in Reflection]
my_tauto.atomics [variable, in Reflection]
m1 [lemma, in Match]
m2 [lemma, in Match]

N

n [axiom, in Universes]
napp [definition, in InductiveTypes]
Nat [constructor, in DataStruct]
nat [inductive, in InductiveTypes]
Nat [constructor, in MoreDep]
Nat [constructor, in Intensional]
Nat [constructor, in StackMachine]
Nat [constructor, in Subset]
Nat [constructor, in Hoas]
natToString [definition, in Hoas]
nat_btree [inductive, in InductiveTypes]
nat_den [definition, in Generic]
nat_dt [definition, in Generic]
nat_fix [definition, in Generic]
nat_ind' [definition, in InductiveTypes]
nat_ind' [section, in InductiveTypes]
nat_ind'.O_case [variable, in InductiveTypes]
nat_ind'.P [variable, in InductiveTypes]
nat_ind'.S_case [variable, in InductiveTypes]
nat_list [inductive, in InductiveTypes]
nat_tree [inductive, in InductiveTypes]
nat_tree_ind' [section, in InductiveTypes]
nat_tree_ind' [definition, in InductiveTypes]
nat_tree_ind'.NLeaf'_case [variable, in InductiveTypes]
nat_tree_ind'.NNode'_case [variable, in InductiveTypes]
nat_tree_ind'.P [variable, in InductiveTypes]
NCons [constructor, in InductiveTypes]
NConst [constructor, in DataStruct]
NConst [constructor, in MoreDep]
Next [constructor, in DataStruct]
Next_cong [lemma, in DeBruijn]
Nil [constructor, in DataStruct]
Nil [constructor, in InductiveTypes]
Nil [constructor, in InductiveTypes]
Nil [constructor, in MoreDep]
NLeaf [constructor, in InductiveTypes]
NLeaf' [constructor, in InductiveTypes]
nlength [definition, in InductiveTypes]
nlength_napp [lemma, in InductiveTypes]
NNil [constructor, in InductiveTypes]
NNode [constructor, in InductiveTypes]
NNode' [constructor, in InductiveTypes]
Node [constructor, in DataStruct]
Node [constructor, in Generic]
Node [constructor, in DataStruct]
None_Some [lemma, in Intensional]
nonrecursive [projection, in Generic]
Not [constructor, in Hoas]
not [definition, in InductiveTypes]
not' [definition, in InductiveTypes]
not_classic [axiom, in Universes]
not_ineq [lemma, in InductiveTypes]
not_inverse [lemma, in InductiveTypes]
nsize [definition, in InductiveTypes]
nsize_nsplice [lemma, in InductiveTypes]
nsplice [definition, in InductiveTypes]
ntsize [definition, in InductiveTypes]
ntsize_ntsplice [lemma, in InductiveTypes]
ntsplice [definition, in InductiveTypes]
nzf [lemma, in DeBruijn]
n_plus_O [lemma, in InductiveTypes]
n_plus_O' [lemma, in InductiveTypes]

O

O [constructor, in InductiveTypes]
oapp [definition, in InductiveTypes]
obvious [lemma, in Predicates]
obvious' [lemma, in Predicates]
OCons [constructor, in InductiveTypes]
odd_list [inductive, in InductiveTypes]
odd_list_mut' [definition, 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]
one [definition, in Hoas]
ones [definition, in Coinductive]
OneStep [constructor, in Hoas]
ones' [definition, in Coinductive]
ones_eq [lemma, in Coinductive]
ones_eq [lemma, in Coinductive]
ones_eq [lemma, in Coinductive]
ones_eq' [lemma, in Coinductive]
one_again [definition, in Hoas]
Op [constructor, in Reflection]
OpSem [library]
Or [constructor, in Reflection]
Or [constructor, in Predicates]
Or [constructor, in Hoas]
Or [constructor, in MoreDep]
Or' [constructor, in Predicates]
or_assoc [lemma, in Predicates]
or_comm [lemma, in Predicates]
or_comm' [lemma, in Predicates]
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]
partialOut [definition, in Reflection]
Phoas [module, in Intensional]
phoasify [section, in Intensional]
Phoasify [definition, in Intensional]
phoasify [definition, in Intensional]
phoasify.var [variable, in Intensional]
phoasify_sound [lemma, in Intensional]
phoasify_wf [lemma, in Intensional]
Phoasify_wf [lemma, in Intensional]
Phoas.Abs [constructor, in Intensional]
Phoas.App [constructor, in Intensional]
Phoas.Const [constructor, in Intensional]
Phoas.EqAbs [constructor, in Intensional]
Phoas.EqApp [constructor, in Intensional]
Phoas.EqConst [constructor, in Intensional]
Phoas.EqPlus [constructor, in Intensional]
Phoas.EqVar [constructor, in Intensional]
Phoas.exp [inductive, in Intensional]
Phoas.Exp [definition, in Intensional]
Phoas.expDenote [definition, in Intensional]
Phoas.ExpDenote [definition, in Intensional]
Phoas.exp_equiv [inductive, in Intensional]
Phoas.exp_equiv [section, in Intensional]
Phoas.exp_equiv.var1 [variable, in Intensional]
Phoas.exp_equiv.var2 [variable, in Intensional]
Phoas.Plus [constructor, in Intensional]
Phoas.Var [constructor, in Intensional]
Phoas.vars [section, in Intensional]
Phoas.vars.var [variable, in Intensional]
Phoas.Wf [definition, in Intensional]
PI [constructor, in Generic]
plug [definition, in Hoas]
Plus [constructor, in DataStruct]
Plus [constructor, in Subset]
Plus [definition, in Hoas]
Plus [constructor, in Large]
Plus [constructor, in MoreDep]
plus [definition, in InductiveTypes]
Plus [constructor, in Large]
Plus [constructor, in StackMachine]
PlusCong1 [constructor, in Hoas]
PlusCong2 [constructor, in Hoas]
Plus' [constructor, in Hoas]
plus1 [lemma, in Universes]
plus_assoc [lemma, in InductiveTypes]
plus_ge [lemma, in DataStruct]
plus_n_Sm' [lemma, in MoreDep]
plus_S [lemma, in InductiveTypes]
positive [axiom, in Universes]
pred [definition, in InductiveTypes]
Predicates [library]
predicate_extensionality [lemma, in Universes]
pred' [definition, in Equality]
pred_strong1 [definition, in Universes]
pred_strong1 [definition, in Subset]
pred_strong1_irrel [lemma, in Universes]
pred_strong1_irrel' [lemma, in Universes]
pred_strong2 [definition, in Subset]
pred_strong3 [definition, in Subset]
pred_strong4 [definition, in Subset]
pred_strong5 [definition, in Subset]
pred_strong6 [definition, in Subset]
pred_strong7 [definition, in Subset]
pred_strong8 [definition, in Subset]
present [definition, in MoreDep]
present [section, in MoreDep]
present.x [variable, in MoreDep]
present_balance1 [lemma, in MoreDep]
present_balance2 [lemma, in MoreDep]
present_ins [lemma, in MoreDep]
present_insert_Black [lemma, in MoreDep]
present_insert_Red [lemma, in MoreDep]
present_insResult [definition, in MoreDep]
print [definition, in Generic]
printName [projection, in Generic]
printNonrec [projection, in Generic]
print_constructor [record, in Generic]
print_datatype [definition, in Generic]
print_nat [definition, in Generic]
Prod [constructor, in MoreDep]
prod' [inductive, in Universes]
prog [definition, in StackMachine]
progDenote [definition, in StackMachine]
progress [lemma, in Hoas]
progress' [lemma, in Hoas]
projS [definition, in Universes]
prop [inductive, in Predicates]
prop [inductive, in Hoas]
propDenote [definition, in Hoas]
propify [definition, in Predicates]
propify_holds [lemma, in Predicates]
propify_holds' [lemma, in Predicates]
propositional [section, in Match]
propositional [lemma, in Match]
Propositional [section, in Predicates]
propositional.P [variable, in Match]
Propositional.P [variable, in Predicates]
Propositional.Q [variable, in Predicates]
propositional.Q [variable, in Match]
propositional.R [variable, in Match]
Propositional.R [variable, in Predicates]
prop' [inductive, in Predicates]
PSLC [module, in Interps]
PSLC.Abs [constructor, in Interps]
PSLC.App [constructor, in Interps]
PSLC.Arrow [constructor, in Interps]
PSLC.Cfold [definition, in Interps]
PSLC.cfold [definition, in Interps]
PSLC.cfold [section, in Interps]
PSLC.cfold.var [variable, in Interps]
PSLC.Cfold_correct [lemma, in Interps]
PSLC.cfold_correct [lemma, in Interps]
PSLC.Const [constructor, in Interps]
PSLC.Exp [definition, in Interps]
PSLC.exp [inductive, in Interps]
PSLC.expDenote [definition, in Interps]
PSLC.ExpDenote [definition, in Interps]
PSLC.Fst [constructor, in Interps]
PSLC.Inl [constructor, in Interps]
PSLC.Inr [constructor, in Interps]
PSLC.Nat [constructor, in Interps]
PSLC.natOut [definition, in Interps]
PSLC.natOut_ns1 [definition, in Interps]
PSLC.natOut_ns2 [definition, in Interps]
PSLC.ns1 [definition, in Interps]
PSLC.ns2 [definition, in Interps]
PSLC.Pair [constructor, in Interps]
PSLC.pairOut [definition, in Interps]
PSLC.pairOutDefault [definition, in Interps]
PSLC.pairOutType [definition, in Interps]
PSLC.pairs [section, in Interps]
PSLC.pairs.A [variable, in Interps]
PSLC.pairs.B [variable, in Interps]
PSLC.pairs.v [variable, in Interps]
PSLC.pairs.v1 [variable, in Interps]
PSLC.pairs.v2 [variable, in Interps]
PSLC.pair_eta1 [lemma, in Interps]
PSLC.pair_eta2 [lemma, in Interps]
PSLC.Plus [constructor, in Interps]
PSLC.Prod [constructor, in Interps]
PSLC.Snd [constructor, in Interps]
PSLC.Sum [constructor, in Interps]
PSLC.SumCase [constructor, in Interps]
PSLC.swap [definition, in Interps]
PSLC.swap_zo [definition, in Interps]
PSLC.type [inductive, in Interps]
PSLC.typeDenote [definition, in Interps]
PSLC.Var [constructor, in Interps]
PSLC.vars [section, in Interps]
PSLC.vars.var [variable, in Interps]
PSLC.zo [definition, in Interps]
push [lemma, in OpSem]

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]
reg [definition, in Coinductive]
regexp [inductive, in MoreDep]
regs [definition, in Coinductive]
rewr [lemma, in Large]
rifoldr [section, in DataStruct]
rifoldr [definition, in DataStruct]
rifoldr.A [variable, in DataStruct]
rifoldr.B [variable, in DataStruct]
rifoldr.f [variable, in DataStruct]
rifoldr.i [variable, in DataStruct]
rpresent [definition, in MoreDep]
rtree [inductive, in MoreDep]

S

S [constructor, in InductiveTypes]
SAbs [constructor, in Hoas]
safe [section, in Coinductive]
safe [inductive, in Coinductive]
safe.prog [variable, in Coinductive]
SApp [constructor, in Hoas]
SConst [constructor, in Hoas]
self_app [definition, in Hoas]
self_app [definition, in Hoas]
self_app' [definition, in Hoas]
set [definition, in Coinductive]
size [definition, in Generic]
size_positive [lemma, in Generic]
slow [section, in Large]
slow [lemma, in Large]
slow' [lemma, in Large]
slow.A [variable, in Large]
slow.f [variable, in Large]
slow.H1 [variable, in Large]
slow.H2 [variable, in Large]
slow.H3 [variable, in Large]
slow.P [variable, in Large]
slow.Q [variable, in Large]
slow.R [variable, in Large]
slow.S [variable, in Large]
Snd [constructor, in MoreDep]
somePairs [definition, in DataStruct]
someTypes [definition, in DataStruct]
someValues [definition, in DataStruct]
Some_Some [lemma, in Intensional]
Source [module, in OpSem]
Source [module, in Extensional]
Source.Abs [constructor, in Extensional]
Source.Abs [constructor, in OpSem]
Source.App [constructor, in OpSem]
Source.App [constructor, in Extensional]
Source.app [definition, in Extensional]
Source.app_ident [definition, in Extensional]
Source.app_ident' [definition, in Extensional]
Source.Arrow [constructor, in Extensional]
Source.Bool [constructor, in OpSem]
Source.closure [definition, in OpSem]
Source.closures [definition, in OpSem]
Source.Const [constructor, in Extensional]
Source.EqAbs [constructor, in OpSem]
Source.EqAbs [constructor, in Extensional]
Source.EqApp [constructor, in Extensional]
Source.EqApp [constructor, in OpSem]
Source.EqBool [constructor, in OpSem]
Source.EqConst [constructor, in Extensional]
Source.EqPlus [constructor, in Extensional]
Source.EqVar [constructor, in OpSem]
Source.EqVar [constructor, in Extensional]
Source.EvAbs [constructor, in OpSem]
Source.Eval [definition, in OpSem]
Source.eval [inductive, in OpSem]
Source.EvApp [constructor, in OpSem]
Source.EvBool [constructor, in OpSem]
Source.EvVar [constructor, in OpSem]
Source.exp [inductive, in Extensional]
Source.Exp [definition, in Extensional]
Source.exp [section, in OpSem]
Source.Exp [definition, in OpSem]
Source.exp [inductive, in OpSem]
Source.ExpDenote [definition, in Extensional]
Source.expDenote [definition, in Extensional]
Source.exp.var [variable, in OpSem]
Source.Exp_equiv [axiom, in Extensional]
Source.exp_equiv [section, in Extensional]
Source.exp_equiv [inductive, in Extensional]
Source.exp_equiv [section, in OpSem]
Source.exp_equiv [inductive, in OpSem]
Source.exp_equiv.var1 [variable, in Extensional]
Source.exp_equiv.var1 [variable, in OpSem]
Source.exp_equiv.var2 [variable, in OpSem]
Source.exp_equiv.var2 [variable, in Extensional]
Source.ident [definition, in Extensional]
Source.one [definition, in Extensional]
Source.Plus [constructor, in Extensional]
Source.TNat [constructor, in Extensional]
Source.type [inductive, in Extensional]
Source.typeDenote [definition, in Extensional]
Source.val [inductive, in OpSem]
Source.Var [constructor, in Extensional]
Source.Var [constructor, in OpSem]
Source.vars [section, in Extensional]
Source.vars.var [variable, in Extensional]
Source.VBool [constructor, in OpSem]
Source.VFun [constructor, in OpSem]
Source.Wf [definition, in OpSem]
Source.zero [definition, in Extensional]
Source.zpo [definition, in Extensional]
split [definition, in MoreDep]
split [section, in MoreDep]
split' [definition, in MoreDep]
split.P1 [variable, in MoreDep]
split.P1_dec [variable, in MoreDep]
split.P2 [variable, in MoreDep]
split.P2_dec [variable, in MoreDep]
split.s [variable, in MoreDep]
SPlus [constructor, in Hoas]
stack [definition, in StackMachine]
StackMachine [library]
Star [constructor, in MoreDep]
star [section, in MoreDep]
star [inductive, in MoreDep]
star.P [variable, in MoreDep]
star_app [lemma, in MoreDep]
star_empty [lemma, in MoreDep]
star_inv [lemma, in MoreDep]
star_length_contra [lemma, in MoreDep]
star_length_flip [lemma, in MoreDep]
star_singleton [lemma, in MoreDep]
star_substring_inv [lemma, in MoreDep]
Step [constructor, in Coinductive]
Step [inductive, in Hoas]
STLC [module, in Interps]
STLC.Abs [constructor, in Interps]
STLC.app [definition, in Interps]
STLC.App [constructor, in Interps]
STLC.app_ident [definition, in Interps]
STLC.app_ident' [definition, in Interps]
STLC.Arrow [constructor, in Interps]
STLC.Cfold [definition, in Interps]
STLC.cfold [section, in Interps]
STLC.cfold [definition, in Interps]
STLC.cfold.var [variable, in Interps]
STLC.Cfold_correct [lemma, in Interps]
STLC.cfold_correct [lemma, in Interps]
STLC.Const [constructor, in Interps]
STLC.Exp [definition, in Interps]
STLC.exp [inductive, in Interps]
STLC.ExpDenote [definition, in Interps]
STLC.expDenote [definition, in Interps]
STLC.ident [definition, in Interps]
STLC.Nat [constructor, in Interps]
STLC.one [definition, in Interps]
STLC.Plus [constructor, in Interps]
STLC.type [inductive, in Interps]
STLC.typeDenote [definition, in Interps]
STLC.Var [constructor, in Interps]
STLC.vars [section, in Interps]
STLC.vars.var [variable, in Interps]
STLC.zero [definition, in Interps]
STLC.zpo [definition, in Interps]
stream [inductive, in Coinductive]
stream [section, in Coinductive]
stream.A [variable, in Coinductive]
stream_eq [inductive, in Coinductive]
stream_eq [section, in Coinductive]
Stream_eq [constructor, in Coinductive]
stream_eq.A [variable, in Coinductive]
Subset [library]
Subst [definition, in Hoas]
subst [definition, in DeBruijn]
substring_all [lemma, in MoreDep]
substring_app_fst [lemma, in MoreDep]
substring_app_snd [lemma, in MoreDep]
substring_empty [lemma, in MoreDep]
substring_le [lemma, in MoreDep]
substring_none [lemma, in MoreDep]
substring_self [lemma, in MoreDep]
substring_split [lemma, in MoreDep]
substring_split' [lemma, in MoreDep]
substring_stack [lemma, in MoreDep]
substring_stack' [lemma, in MoreDep]
substring_suffix [lemma, in MoreDep]
substring_suffix_emp [lemma, in MoreDep]
substring_suffix_emp' [lemma, in MoreDep]
substVar [definition, in DeBruijn]
substVar_lift [lemma, in DeBruijn]
substVar_liftVar [lemma, in DeBruijn]
substVar_lift' [lemma, in DeBruijn]
substVar_unliftVar [lemma, in DeBruijn]
subst_comm [lemma, in DeBruijn]
subst_comm' [lemma, in DeBruijn]
sum [definition, in DataStruct]
sum [definition, in DataStruct]
sum [definition, in InductiveTypes]
Sum [constructor, in Hoas]
sum_inc [lemma, in DataStruct]
sum_inc [lemma, in DataStruct]
sum_inc' [lemma, in DataStruct]
swap [definition, in Hoas]
swapper [definition, in InductiveTypes]
swapper_preserves_truth [lemma, in InductiveTypes]
sym_ex [definition, in Universes]
sym_sig [definition, in Universes]
S_eta [lemma, in Equality]
S_inj [lemma, in InductiveTypes]
S_inj' [lemma, in InductiveTypes]
S_isZero [lemma, in InductiveTypes]

T

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]
tbinop [inductive, in StackMachine]
TBinop [constructor, in StackMachine]
tbinopDenote [definition, 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_inster [section, in Match]
test_inster [lemma, in Match]
test_inster.A [variable, in Match]
test_inster.f [variable, in Match]
test_inster.g [variable, in Match]
test_inster.H1 [variable, in Match]
test_inster.H3 [variable, in Match]
test_inster.H4 [variable, in Match]
test_inster.P [variable, in Match]
test_inster.Q [variable, in Match]
test_inster2 [lemma, in Match]
texp [inductive, in StackMachine]
texpDenote [definition, in StackMachine]
the_sky_is_falling [lemma, in InductiveTypes]
TIBConst [constructor, in StackMachine]
TIBinop [constructor, in StackMachine]
Times [constructor, in StackMachine]
times [definition, in Large]
times [definition, in Large]
times [definition, in Large]
times [definition, in Large]
TINConst [constructor, in StackMachine]
tinstr [inductive, in StackMachine]
tinstrDenote [definition, in StackMachine]
TLt [constructor, in StackMachine]
TNat [constructor, in Subset]
TNConst [constructor, in StackMachine]
TNil [constructor, in StackMachine]
toString [definition, in Hoas]
ToString [definition, in Hoas]
ToString [section, in Hoas]
TPlus [constructor, in StackMachine]
tprog [inductive, in StackMachine]
tprogDenote [definition, in StackMachine]
tree [inductive, in DataStruct]
tree [section, in Generic]
tree [inductive, in Generic]
tree [section, in DataStruct]
tree [section, in DataStruct]
tree [inductive, in DataStruct]
tree.A [variable, in DataStruct]
tree.A [variable, in Generic]
tree.A [variable, in DataStruct]
tree_den [definition, in Generic]
tree_dt [definition, in Generic]
tree_fix [definition, in Generic]
Tru [constructor, in Predicates]
true [constructor, in InductiveTypes]
trues [definition, in Coinductive]
True_conc [lemma, in Match]
true_galore [lemma, in Reflection]
true_galore' [lemma, in Reflection]
true_neq_false [lemma, in InductiveTypes]
true_prop [definition, in Hoas]
Truth [constructor, in Reflection]
Tru' [constructor, in Predicates]
tstack [definition, in StackMachine]
tt [constructor, in InductiveTypes]
TTimes [constructor, in StackMachine]
twoEls [section, in Predicates]
TwoEls [constructor, in Predicates]
twoEls [inductive, in Predicates]
twoEls.A [variable, in Predicates]
twoEls_nil [lemma, in Predicates]
twoEls_two [lemma, in Predicates]
type [inductive, in Subset]
type [inductive, in StackMachine]
type [inductive, in Intensional]
type [inductive, in Hoas]
type [inductive, in MoreDep]
type [inductive, in DataStruct]
typeCheck [definition, in Subset]
typeCheck' [definition, in Subset]
typeDenote [definition, in DataStruct]
typeDenote [definition, in StackMachine]
typeDenote [definition, in Intensional]
typeDenote [definition, in MoreDep]
type' [inductive, in DataStruct]
type'Denote [definition, in DataStruct]
t1 [lemma, in Reflection]
t1 [lemma, in Universes]
t1 [lemma, in Match]
t1' [lemma, in Match]
t2 [lemma, in Match]
t2 [lemma, in Universes]
t2' [lemma, in Universes]
t3 [lemma, in Universes]
t3 [lemma, in Universes]
t3 [lemma, in Match]
t4 [lemma, in Universes]
t4 [lemma, in Match]
t5 [lemma, in Match]
t5' [lemma, in Match]
t6 [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 [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

UAbs [constructor, in Hoas]
UAbs [constructor, in Hoas]
UAbs [constructor, in Hoas]
UApp [constructor, in Hoas]
UApp [constructor, in Hoas]
UApp [constructor, in Hoas]
Uexp [definition, in Hoas]
uexp [section, in Hoas]
uexp [inductive, in Hoas]
uexp [inductive, in Hoas]
uexp [inductive, in Hoas]
uexp.var [variable, in Hoas]
uhoh [lemma, in Universes]
uhoh_again [lemma, in Universes]
UIP [lemma, in Universes]
UIP_refl [lemma, in Universes]
UIP_refl' [definition, in Equality]
UIP_refl'' [lemma, in Equality]
undo_lift [lemma, in DeBruijn]
undo_lift' [lemma, in DeBruijn]
unique_ident [lemma, in Large]
Unit [constructor, in DataStruct]
unit [inductive, in InductiveTypes]
unit_den [definition, in Generic]
unit_dt [definition, in Generic]
unit_fix [definition, in Generic]
unit_rect' [definition, in InductiveTypes]
unit_singleton [lemma, in InductiveTypes]
Universes [library]
unject [definition, in MoreDep]
Unknown [constructor, in Subset]
unliftVar [definition, in DeBruijn]
unsimpl_zip [lemma, in Intensional]
UVar [constructor, in Hoas]
UVar [constructor, in Hoas]
UVar [constructor, in Hoas]

V

VAbs [constructor, in Hoas]
VAbs [constructor, in OpSem]
val [inductive, in OpSem]
val [section, in OpSem]
Val [inductive, in Hoas]
val.var [variable, in OpSem]
Val_Big [lemma, in Hoas]
Var [constructor, in DeBruijn]
Var [constructor, in Reflection]
Var [constructor, in OpSem]
Var [constructor, in DataStruct]
var [axiom, in Hoas]
Var [constructor, in Hoas]
vars [section, in Intensional]
vars.var1 [variable, in Intensional]
vars.var2 [variable, in Intensional]
vars_easy [lemma, in Extensional]
VConst [constructor, in Hoas]
vstack [definition, in StackMachine]