Global Index

A

Abs [constructor, in Impure]
Abs [constructor, in DataStruct]
Abs [definition, in Hoas]
Abs' [constructor, in Hoas]
Add [constructor, in Coinductive]
add [definition, in Reflection]
add_self [definition, in Hoas]
All [definition, in InductiveTypes]
allTrue [definition, in Reflection]
allTrue_add [lemma, in Reflection]
allTrue_In [lemma, in Reflection]
always_O [definition, in InductiveTypes]
always_O' [definition, in InductiveTypes]
And [constructor, in Reflection]
And [constructor, in InductiveTypes]
And [constructor, in Subset]
And [constructor, in MoreDep]
and_comm [lemma, in Predicates]
and_True_conc [lemma, in Match]
and_True_prem [lemma, in Match]
App [definition, in Hoas]
app [definition, in MoreDep]
app [definition, in InductiveTypes]
app [definition, in InductiveTypes]
App [constructor, in DataStruct]
app [definition, in Hoas]
App [constructor, in Impure]
AppCong1 [constructor, in Hoas]
AppCong2 [constructor, in Hoas]
approx [definition, in Coinductive]
App' [constructor, in Hoas]
app_first [definition, in Intensional]
app_first_ok [lemma, in Intensional]
app_ident [definition, in Hoas]
app_ident [definition, in Intensional]
app_ident' [definition, in Hoas]
app_ident1 [definition, in Hoas]
app_ident_ok [lemma, in Intensional]
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 Hoas]
Arrow [constructor, in DataStruct]
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]

B

backward [definition, in Reflection]
balanced [lemma, in MoreDep]
balance1 [definition, in MoreDep]
balance2 [definition, in MoreDep]
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 [constructor, in StackMachine]
binop [inductive, in StackMachine]
binopDenote [definition, in StackMachine]
Black [constructor, in MoreDep]
BlackNode [constructor, in MoreDep]
Bool [constructor, in MoreDep]
bool [inductive, in InductiveTypes]
Bool [constructor, in Subset]
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

D

E

eapp [definition, in InductiveTypes]
ECons [constructor, in InductiveTypes]
Elab [module, in Extensional]
elength [definition, in InductiveTypes]
elength_eapp [lemma, in InductiveTypes]
elength_eapp [lemma, in InductiveTypes]
empty [definition, in Coinductive]
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]
end [definition, in DataStruct]
end [definition, in DataStruct]
end [definition, in Equality]
ENil [constructor, in InductiveTypes]
envOf [definition, in Intensional]
envType [definition, in Intensional]
env_prog [definition, in Intensional]
Eq [constructor, in DataStruct]
Eq [constructor, in MoreDep]
Eq [constructor, in InductiveTypes]
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]
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_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]
exist1 [lemma, in Predicates]
exist2 [lemma, in Predicates]
exp [inductive, in MoreDep]
Exp [definition, in Hoas]
exp [inductive, in StackMachine]
exp [inductive, in Hoas]
exp [inductive, in Subset]
exp [inductive, in DataStruct]
expDenote [definition, in StackMachine]
expDenote [definition, in MoreDep]
expDenote [definition, in DataStruct]
exp' [inductive, in DataStruct]
exp'Denote [definition, in DataStruct]
Exp1 [definition, in Hoas]
Exp_equiv [axiom, in Extensional]
Exp_equiv [axiom, in Intensional]
Exp_wf [lemma, in Intensional]
Exp_wf' [lemma, in Intensional]
Extensional [library]
ext_eq [axiom, in Equality]
ex_conc [lemma, in Match]
ex_prem [lemma, in Match]
e2u [definition, in InductiveTypes]

F

f [definition, in InductiveTypes]
false [constructor, in InductiveTypes]
Falsehood [constructor, in Reflection]
falses [definition, in Coinductive]
False_imp [lemma, in Predicates]
False_prem [lemma, in Match]
fget [definition, in DataStruct]
fhapp [definition, in Equality]
fhapp_ass [lemma, in Equality]
fhapp_ass' [lemma, in Equality]
fhget [definition, in DataStruct]
fhget [definition, in Equality]
fhlist [definition, in Equality]
fhlist [definition, in DataStruct]
fhmap [definition, in Equality]
filist [definition, in DataStruct]
findex [definition, in DataStruct]
first [definition, in Intensional]
First [constructor, in DataStruct]
Firstorder [library]
first_ok [lemma, in Intensional]
fixDenote [definition, in Generic]
fixDenoteOk [definition, in Generic]
flatten [definition, in Reflection]
flatten [definition, in Hoas]
flatten_correct [lemma, in Reflection]
flatten_correct' [lemma, in Reflection]
fmember [definition, in DataStruct]
fmember [definition, in Equality]
fo [lemma, in Match]
foldr_plus [lemma, in Generic]
Forall [constructor, in InductiveTypes]
forall_and [lemma, in Match]
forall_eq [lemma, in Equality]
formula [inductive, in Reflection]
formula [inductive, in InductiveTypes]
formulaDenote [definition, in InductiveTypes]
formulaDenote [definition, in Reflection]
formula_ind' [definition, 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]
fvsExp [definition, in Intensional]
fvsExp_correct [lemma, in Intensional]
fvsExp_minimal [lemma, in Intensional]
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

Generic [library]
get [definition, in DataStruct]
get [definition, in Coinductive]
get_imap [lemma, in DataStruct]
get_imap [lemma, in Equality]

H

Halt [constructor, in Coinductive]
hasType [inductive, in Subset]
hasType_det [lemma, in Subset]
hd [definition, in MoreDep]
hd' [definition, in MoreDep]
hget [definition, in DataStruct]
hlist [inductive, in DataStruct]
hmm [lemma, in Match]
hmm' [lemma, in Match]
hmm2 [lemma, in Match]
Hoas [library]
holds [definition, in Reflection]
HtAnd [constructor, in Subset]
HtBool [constructor, in Subset]
HtNat [constructor, in Subset]
HtPlus [constructor, in Subset]

I

IBinop [constructor, in StackMachine]
IConst [constructor, in StackMachine]
ident [definition, in Hoas]
ident [definition, in Impure]
Ident [constructor, in Reflection]
ident [definition, in Intensional]
ident1 [definition, in Hoas]
ident_ok [lemma, in Intensional]
ident_self [definition, in Impure]
ident_unit [definition, in Impure]
If [constructor, in MoreDep]
ifoldr [definition, in DataStruct]
ilist [inductive, in DataStruct]
ilist [inductive, in MoreDep]
imap [definition, in DataStruct]
Imp [constructor, in Reflection]
imp [definition, in Reflection]
imp [definition, in Match]
impredicative [module, in Impure]
impredicative.Bind [constructor, in Impure]
impredicative.computation [inductive, in Impure]
impredicative.Dyn [constructor, in Impure]
impredicative.dynamic [inductive, in Impure]
impredicative.eval [inductive, in Impure]
impredicative.EvalBind [constructor, in Impure]
impredicative.EvalReturn [constructor, in Impure]
impredicative.EvalUnpack [constructor, in Impure]
impredicative.eval_ident_unit [lemma, in Impure]
impredicative.invert_ident [lemma, in Impure]
impredicative.Return [constructor, in Impure]
impredicative.TermDenote [definition, in Impure]
impredicative.termDenote [definition, in Impure]
impredicative.Unpack [constructor, in Impure]
Impure [library]
imp_True [lemma, in Match]
inc [definition, in DataStruct]
inc [definition, in DataStruct]
inclusion [lemma, in Intensional]
index [inductive, 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]
insertResult [definition, in MoreDep]
insResult [definition, in MoreDep]
instr [inductive, in StackMachine]
instrDenote [definition, in StackMachine]
instrs [inductive, in Coinductive]
Intensional [library]
interleave [definition, in Coinductive]
Interps [library]
Intro [library]
In_dec [definition, in Subset]
In_dec [definition, in Reflection]
in_star [lemma, in Match]
IsApp1 [constructor, in Hoas]
IsApp2 [constructor, in Hoas]
isCtx [inductive, in Hoas]
isEven [inductive, in Reflection]
isfree [definition, in Intensional]
isfree_merge [definition, in Intensional]
isfree_merge_correct1 [lemma, in Intensional]
isfree_merge_correct2 [lemma, in Intensional]
isfree_none [definition, in Intensional]
isfree_one [definition, in Intensional]
isfree_one_correct [lemma, in Intensional]
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

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

L

M

makeEnv [definition, in Intensional]
makeRbtree [definition, in MoreDep]
map [definition, in Coinductive]
map [definition, in Generic]
map [definition, in InductiveTypes]
map_funcs [definition, in Intensional]
map_funcs_correct [lemma, in Intensional]
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]
mldenote [definition, in Reflection]
MNext [constructor, in DataStruct]
MNil [constructor, in DataStruct]
monoid_reflect [lemma, in Reflection]
MoreDep [library]
mt1 [lemma, in Reflection]
mt2 [lemma, in Reflection]
mt3 [lemma, in Reflection]
mt4 [lemma, in Reflection]
mt4' [lemma, in Reflection]
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]
m1 [lemma, in Match]
m2 [lemma, in Match]

N

napp [definition, in InductiveTypes]
Nat [constructor, in StackMachine]
Nat [constructor, in DataStruct]
Nat [constructor, in Subset]
nat [inductive, in InductiveTypes]
Nat [constructor, in Hoas]
Nat [constructor, in MoreDep]
natToString [definition, in Hoas]
natvar [definition, in Intensional]
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_list [inductive, in InductiveTypes]
nat_tree [inductive, in InductiveTypes]
nat_tree_ind' [definition, in InductiveTypes]
NCons [constructor, in InductiveTypes]
NConst [constructor, in MoreDep]
NConst [constructor, in DataStruct]
Next [constructor, in DataStruct]
Nil [constructor, in MoreDep]
Nil [constructor, in DataStruct]
Nil [constructor, in InductiveTypes]
Nil [constructor, in InductiveTypes]
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]
not [definition, in InductiveTypes]
not' [definition, in InductiveTypes]
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]
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]
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]
Or [constructor, in MoreDep]
Or [constructor, in Reflection]
or_comm [lemma, in Predicates]
or_comm' [lemma, in Predicates]
O_plus_n [lemma, in InductiveTypes]

P

R

RAdd [constructor, in Coinductive]
rbtree [inductive, in MoreDep]
RConst [constructor, in Coinductive]
Red [constructor, in MoreDep]
RedNode [constructor, in MoreDep]
RedNode' [constructor, in MoreDep]
reduce_me [lemma, in Equality]
Reflection [library]
reg [inductive, in Coinductive]
regexp [inductive, in MoreDep]
regmap [inductive, in Coinductive]
regmapCompat [definition, in Coinductive]
regmapCompat_set_None [lemma, in Coinductive]
regmapCompat_set_Some [lemma, in Coinductive]
RHalt [constructor, in Coinductive]
rifoldr [definition, in DataStruct]
RJeq_eq [constructor, in Coinductive]
RJeq_neq [constructor, in Coinductive]
rpresent [definition, in MoreDep]
rtree [inductive, in MoreDep]
run [inductive, in Coinductive]
R1 [constructor, in Coinductive]
R2 [constructor, in Coinductive]

S

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]
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]
term [inductive, in Impure]
Term [definition, in Impure]
test_inster [lemma, 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]
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]
TPlus [constructor, in StackMachine]
tprog [inductive, in StackMachine]
tprogDenote [definition, in StackMachine]
tree [inductive, in DataStruct]
tree [inductive, in DataStruct]
tree [inductive, in Generic]
tree_den [definition, in Generic]
tree_dt [definition, in Generic]
tree_fix [definition, in Generic]
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]
Truth [constructor, in Reflection]
tstack [definition, in StackMachine]
tt [constructor, in InductiveTypes]
TTimes [constructor, in StackMachine]
type [inductive, in Subset]
type [inductive, in DataStruct]
type [inductive, in Hoas]
type [inductive, in StackMachine]
type [inductive, in MoreDep]
typeCheck [definition, in Subset]
typeCheck' [definition, in Subset]
typeDenote [definition, in MoreDep]
typeDenote [definition, in StackMachine]
typeDenote [definition, in DataStruct]
typeDenote_same [lemma, in Intensional]
type' [inductive, in DataStruct]
type'Denote [definition, in DataStruct]
t1 [lemma, in Reflection]
t1 [lemma, in Match]
t1' [lemma, in Match]
t2 [lemma, in Match]
t3 [lemma, in Match]
t4 [lemma, in Match]

U

UIP_refl' [definition, in Equality]
UIP_refl'' [lemma, in Equality]
Unit [constructor, in DataStruct]
Unit [constructor, in Impure]
unit [inductive, in InductiveTypes]
unite [definition, in Impure]
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]
unject [definition, in MoreDep]
Unknown [constructor, in Subset]
unpackExp [definition, in Intensional]
unpackExp_correct [lemma, in Intensional]

V

VAbs [constructor, in Hoas]
Val [inductive, in Hoas]
Val_Big [lemma, in Hoas]
Var [constructor, in DataStruct]
Var [constructor, in Hoas]
Var [constructor, in Reflection]
Var [constructor, in Impure]
VConst [constructor, in Hoas]
vstack [definition, in StackMachine]