Global Index

other

(327 entries)

Notation Index

other

(5 entries)

Binder Index

other

(195 entries)

Module Index

other

(3 entries)

Library Index

other

(9 entries)

Lemma Index

other

(29 entries)

Constructor Index

other

(5 entries)

Axiom Index

other

(26 entries)

Inductive Index

other

(2 entries)

Section Index

other

(1 entry)

Definition Index

other

(52 entries)

Global Index

A

B

C

C [axiom, in Top.TestEquality]
c [definition, in Top.TestEquality]
construct_tuple_lemma [lemma, in Top.TestEquality3]
C:27 [binder, in Top.Helpers]
C:31 [binder, in Top.Helpers]
C:35 [binder, in Top.Helpers]
C:4 [binder, in Top.TestEquality3]
C:45 [binder, in Top.Helpers]
C:50 [binder, in Top.Helpers]
C:9 [binder, in Top.Helpers]

D

data [axiom, in Top.Library]
diff [axiom, in Top.Library]
drhs:33 [binder, in Top.TestHelpers]
ds:30 [binder, in Top.TestHelpers]
D:14 [binder, in Top.TestHelpers]
d:27 [binder, in Top.TestHelpers]
D:46 [binder, in Top.Helpers]
D:5 [binder, in Top.TestEquality3]
D:51 [binder, in Top.Helpers]

E

F

fst_v [axiom, in Top.Library]
f:2 [binder, in Top.Translation]
f:47 [binder, in Top.TestHelpers]
f:6 [binder, in Top.Translation]

G

GC [axiom, in Top.Library]
GenArgT [definition, in Top.Library]
GenT [axiom, in Top.Library]
get_term [definition, in Top.Predefs]
GN [axiom, in Top.Library]
gngc_simple [axiom, in Top.TestEqualityEnv]
G:1 [binder, in Top.Helpers]
G:1 [binder, in Top.RuleTests]
G:1 [binder, in Top.TestEquality3]
G:10 [binder, in Top.Helpers]
G:13 [binder, in Top.Helpers]
G:15 [binder, in Top.Helpers]
G:20 [binder, in Top.Helpers]
G:20 [binder, in Top.RuleTests]
G:20 [binder, in Top.Library]
G:24 [binder, in Top.Helpers]
G:27 [binder, in Top.RuleTests]
G:28 [binder, in Top.Helpers]
G:30 [binder, in Top.RuleTests]
G:32 [binder, in Top.Helpers]
G:36 [binder, in Top.Helpers]
G:39 [binder, in Top.Helpers]
G:39 [binder, in Top.RuleTests]
G:42 [binder, in Top.Helpers]
G:47 [binder, in Top.Helpers]
G:52 [binder, in Top.Helpers]
G:54 [binder, in Top.Helpers]
G:56 [binder, in Top.Helpers]
G:58 [binder, in Top.Helpers]
G:6 [binder, in Top.Helpers]
G:61 [binder, in Top.Helpers]
G:64 [binder, in Top.Helpers]
G:8 [binder, in Top.RuleTests]

H

has_only_objects_or_top [inductive, in Top.RuleTests]
Helpers [library]
Htyp:5 [binder, in Top.Predefs]

I

inner:55 [binder, in Top.TestHelpers]
internalTupleTyp [definition, in Top.Library]
intersection_order [lemma, in Top.Helpers]
i:11 [binder, in Top.TestEqualityEnv]
i:3 [binder, in Top.TestEqualityEnv]
i:5 [binder, in Top.TestEqualityEnv]
i:8 [binder, in Top.TestEqualityEnv]

J

j:12 [binder, in Top.TestEqualityEnv]
j:6 [binder, in Top.TestEqualityEnv]
j:9 [binder, in Top.TestEqualityEnv]

K

k:1 [binder, in Top.TestHelpers]
k:12 [binder, in Top.TestHelpers]
k:19 [binder, in Top.TestHelpers]
k:22 [binder, in Top.TestHelpers]
k:25 [binder, in Top.TestHelpers]
k:28 [binder, in Top.TestHelpers]
k:31 [binder, in Top.TestHelpers]
k:5 [binder, in Top.TestHelpers]
k:9 [binder, in Top.TestHelpers]

L

lib [definition, in Top.Library]
libInternalType [definition, in Top.Library]
libPreType [definition, in Top.Library]
libPreTypeHelp [definition, in Top.Library]
Library [library]
libTrm [definition, in Top.Library]
libType [definition, in Top.Library]
libTypes [lemma, in Top.Library]
lib:17 [binder, in Top.TestEqualityEnv]
lib:38 [binder, in Top.RuleTests]
lift_rec_defrhs [definition, in Top.TestHelpers]
lift_rec_defs [definition, in Top.TestHelpers]
lift_rec_def [definition, in Top.TestHelpers]
lift_rec_val [definition, in Top.TestHelpers]
lift_rec_trm [definition, in Top.TestHelpers]
lift_rec_dec [definition, in Top.TestHelpers]
lift_rec_typ [definition, in Top.TestHelpers]
lift_rec_path [definition, in Top.TestHelpers]
lift_rec_avar [definition, in Top.TestHelpers]
l':11 [binder, in Top.Translation]
l:17 [binder, in Top.Translation]
L:18 [binder, in Top.Helpers]
l:5 [binder, in Top.Translation]
l:7 [binder, in Top.Translation]

M

make_fun_apply [definition, in Top.TestHelpers]
mkTuple [axiom, in Top.Library]
mkUnit [axiom, in Top.Library]

N

neq_lib_env [lemma, in Top.Library]
n':10 [binder, in Top.Translation]
n:16 [binder, in Top.Translation]
n:4 [binder, in Top.Translation]

O

obj_only_eq_and_rule_would_be_unsound [lemma, in Top.RuleTests]
offset:17 [binder, in Top.Library]
only_and [constructor, in Top.RuleTests]
only_typ [constructor, in Top.RuleTests]
only_val [constructor, in Top.RuleTests]
only_top [constructor, in Top.RuleTests]
open1 [definition, in Top.Translation]

P

pmatch [axiom, in Top.Library]
pmatch_data [axiom, in Top.TestEqualityEnv]
Predefs [library]
p_transitivity_types [lemma, in Top.TestEquality]
p_transitivity_trm [definition, in Top.TestEquality]
p_transitivity_typ [definition, in Top.TestEquality]
p_coerce_types [lemma, in Top.TestEquality]
p_coerce_trm [definition, in Top.TestEquality]
p_coerce_typ [definition, in Top.TestEquality]
p_construct_types [lemma, in Top.TestEquality3]
p_construct_trm [definition, in Top.TestEquality3]
p_construct_typ [definition, in Top.TestEquality3]
p:21 [binder, in Top.Helpers]
p:46 [binder, in Top.TestHelpers]
p:7 [binder, in Top.TestHelpers]

R

ref [definition, in Top.Library]
refl [axiom, in Top.TestEqualityEnv]
res:29 [binder, in Top.Translation]
retT:6 [binder, in Top.TestEquality3]
RuleTests [library]
R:6 [binder, in Top.Predefs]

S

shift1_p [definition, in Top.TestHelpers]
shift1_trm [definition, in Top.TestHelpers]
shift1_typ [definition, in Top.TestHelpers]
simple_eq_and_rule_would_be_unsound [lemma, in Top.RuleTests]
skip1 [definition, in Top.Translation]
snd_v [axiom, in Top.Library]
snglhelper [axiom, in Top.TestEqualityEnv]
Source [module, in Top.Predefs]
SourceAnnot [module, in Top.Predefs]
sub [definition, in Top.TestEquality]
sub_exfalso [lemma, in Top.Helpers]
sub_and_merge [lemma, in Top.Helpers]
sub_and_comm [lemma, in Top.Helpers]
sub_and_assoc2 [lemma, in Top.Helpers]
sub_and_assoc [lemma, in Top.Helpers]
swap_typ [lemma, in Top.Helpers]

T

t [definition, in Top.TestEquality]
Target [module, in Top.Predefs]
TestApp [section, in Top.TestEquality]
TestEquality [library]
TestEqualityEnv [library]
TestEquality3 [library]
TestHelpers [library]
TLgen [definition, in Top.TestHelpers]
translateType [definition, in Top.Translation]
translateTyp0 [definition, in Top.Translation]
Translation [library]
Ts':24 [binder, in Top.Translation]
TT1:21 [binder, in Top.Library]
TT2:22 [binder, in Top.Library]
Tuple [axiom, in Top.Library]
TupleT [definition, in Top.Library]
tupleTyp [definition, in Top.Library]
typed_target_term_cons [constructor, in Top.Predefs]
typed_target_term [inductive, in Top.Predefs]
type_map [definition, in Top.Translation]
ty_map:13 [binder, in Top.Translation]
T1 [axiom, in Top.Library]
T1':18 [binder, in Top.Translation]
T1':20 [binder, in Top.Translation]
T1:18 [binder, in Top.RuleTests]
T1:22 [binder, in Top.Translation]
T2 [axiom, in Top.Library]
T2':19 [binder, in Top.Translation]
T2':21 [binder, in Top.Translation]
T2:19 [binder, in Top.RuleTests]
T:11 [binder, in Top.TestHelpers]
T:12 [binder, in Top.Translation]
T:14 [binder, in Top.RuleTests]
T:16 [binder, in Top.RuleTests]
T:19 [binder, in Top.Helpers]
t:21 [binder, in Top.TestHelpers]
T:23 [binder, in Top.Helpers]
t:23 [binder, in Top.Translation]
T:24 [binder, in Top.RuleTests]
T:27 [binder, in Top.Translation]
t:3 [binder, in Top.Predefs]
T:30 [binder, in Top.Translation]
T:34 [binder, in Top.RuleTests]
T:4 [binder, in Top.Predefs]
t:4 [binder, in Top.TestEquality]
t:44 [binder, in Top.TestHelpers]
t:45 [binder, in Top.TestHelpers]
T:5 [binder, in Top.RuleTests]
t:50 [binder, in Top.TestHelpers]
T:54 [binder, in Top.TestHelpers]

U

Unit [axiom, in Top.Library]
unitDec:18 [binder, in Top.Library]
unitRef:19 [binder, in Top.Library]
Unnamed_thm2 [definition, in Top.TestEquality]
Unnamed_thm1 [definition, in Top.TestEquality]
Unnamed_thm0 [definition, in Top.TestEquality]
Unnamed_thm [definition, in Top.TestEquality]
u:13 [binder, in Top.TestHelpers]
U:17 [binder, in Top.RuleTests]
u:20 [binder, in Top.TestHelpers]
u:23 [binder, in Top.TestHelpers]
U:25 [binder, in Top.RuleTests]
u:26 [binder, in Top.TestHelpers]
u:29 [binder, in Top.TestHelpers]
u:32 [binder, in Top.TestHelpers]
U:35 [binder, in Top.RuleTests]
U:6 [binder, in Top.RuleTests]

V

v:24 [binder, in Top.TestHelpers]

W

weak_uniqueness_eq_and_rule_would_be_unsound [lemma, in Top.RuleTests]
withlet:49 [binder, in Top.TestHelpers]
wrap:51 [binder, in Top.TestHelpers]
w:10 [binder, in Top.TestHelpers]
w:2 [binder, in Top.TestHelpers]
w:6 [binder, in Top.TestHelpers]

X

Y

Y:10 [binder, in Top.RuleTests]
Y:17 [binder, in Top.Helpers]
y:2 [binder, in Top.TestEqualityEnv]
Y:29 [binder, in Top.RuleTests]
Y:41 [binder, in Top.RuleTests]
Y:63 [binder, in Top.Helpers]
Y:66 [binder, in Top.Helpers]

other

_ ⊢ _ =:= _ [notation, in Top.Helpers]
_ $$ _ [notation, in Top.TestHelpers]
_ $ _ [notation, in Top.TestHelpers]
{ _ == _ } [notation, in Top.Helpers]
{( _ , .. , _ )} [notation, in Top.Helpers]

Notation Index

other

_ ⊢ _ =:= _ [in Top.Helpers]
_ $$ _ [in Top.TestHelpers]
_ $ _ [in Top.TestHelpers]
{ _ == _ } [in Top.Helpers]
{( _ , .. , _ )} [in Top.Helpers]

Binder Index

A

B

base:25 [in Top.Translation]
B1:3 [in Top.Helpers]
B2:5 [in Top.Helpers]
B:12 [in Top.Helpers]
B:26 [in Top.Helpers]
B:3 [in Top.TestEquality3]
B:30 [in Top.Helpers]
B:34 [in Top.Helpers]
B:36 [in Top.RuleTests]
B:38 [in Top.Helpers]
B:41 [in Top.Helpers]
B:44 [in Top.Helpers]
B:49 [in Top.Helpers]
B:60 [in Top.Helpers]
B:8 [in Top.Helpers]

C

C:27 [in Top.Helpers]
C:31 [in Top.Helpers]
C:35 [in Top.Helpers]
C:4 [in Top.TestEquality3]
C:45 [in Top.Helpers]
C:50 [in Top.Helpers]
C:9 [in Top.Helpers]

D

drhs:33 [in Top.TestHelpers]
ds:30 [in Top.TestHelpers]
D:14 [in Top.TestHelpers]
d:27 [in Top.TestHelpers]
D:46 [in Top.Helpers]
D:5 [in Top.TestEquality3]
D:51 [in Top.Helpers]

F

f:2 [in Top.Translation]
f:47 [in Top.TestHelpers]
f:6 [in Top.Translation]

G

H

Htyp:5 [in Top.Predefs]

I

inner:55 [in Top.TestHelpers]
i:11 [in Top.TestEqualityEnv]
i:3 [in Top.TestEqualityEnv]
i:5 [in Top.TestEqualityEnv]
i:8 [in Top.TestEqualityEnv]

J

j:12 [in Top.TestEqualityEnv]
j:6 [in Top.TestEqualityEnv]
j:9 [in Top.TestEqualityEnv]

K

k:1 [in Top.TestHelpers]
k:12 [in Top.TestHelpers]
k:19 [in Top.TestHelpers]
k:22 [in Top.TestHelpers]
k:25 [in Top.TestHelpers]
k:28 [in Top.TestHelpers]
k:31 [in Top.TestHelpers]
k:5 [in Top.TestHelpers]
k:9 [in Top.TestHelpers]

L

lib:17 [in Top.TestEqualityEnv]
lib:38 [in Top.RuleTests]
l':11 [in Top.Translation]
l:17 [in Top.Translation]
L:18 [in Top.Helpers]
l:5 [in Top.Translation]
l:7 [in Top.Translation]

N

n':10 [in Top.Translation]
n:16 [in Top.Translation]
n:4 [in Top.Translation]

O

offset:17 [in Top.Library]

P

p:21 [in Top.Helpers]
p:46 [in Top.TestHelpers]
p:7 [in Top.TestHelpers]

R

res:29 [in Top.Translation]
retT:6 [in Top.TestEquality3]
R:6 [in Top.Predefs]

T

Ts':24 [in Top.Translation]
TT1:21 [in Top.Library]
TT2:22 [in Top.Library]
ty_map:13 [in Top.Translation]
T1':18 [in Top.Translation]
T1':20 [in Top.Translation]
T1:18 [in Top.RuleTests]
T1:22 [in Top.Translation]
T2':19 [in Top.Translation]
T2':21 [in Top.Translation]
T2:19 [in Top.RuleTests]
T:11 [in Top.TestHelpers]
T:12 [in Top.Translation]
T:14 [in Top.RuleTests]
T:16 [in Top.RuleTests]
T:19 [in Top.Helpers]
t:21 [in Top.TestHelpers]
T:23 [in Top.Helpers]
t:23 [in Top.Translation]
T:24 [in Top.RuleTests]
T:27 [in Top.Translation]
t:3 [in Top.Predefs]
T:30 [in Top.Translation]
T:34 [in Top.RuleTests]
T:4 [in Top.Predefs]
t:4 [in Top.TestEquality]
t:44 [in Top.TestHelpers]
t:45 [in Top.TestHelpers]
T:5 [in Top.RuleTests]
t:50 [in Top.TestHelpers]
T:54 [in Top.TestHelpers]

U

unitDec:18 [in Top.Library]
unitRef:19 [in Top.Library]
u:13 [in Top.TestHelpers]
U:17 [in Top.RuleTests]
u:20 [in Top.TestHelpers]
u:23 [in Top.TestHelpers]
U:25 [in Top.RuleTests]
u:26 [in Top.TestHelpers]
u:29 [in Top.TestHelpers]
u:32 [in Top.TestHelpers]
U:35 [in Top.RuleTests]
U:6 [in Top.RuleTests]

V

v:24 [in Top.TestHelpers]

W

withlet:49 [in Top.TestHelpers]
wrap:51 [in Top.TestHelpers]
w:10 [in Top.TestHelpers]
w:2 [in Top.TestHelpers]
w:6 [in Top.TestHelpers]

X

X1:2 [in Top.RuleTests]
X1:21 [in Top.RuleTests]
X1:31 [in Top.RuleTests]
X2:22 [in Top.RuleTests]
X2:3 [in Top.RuleTests]
X2:32 [in Top.RuleTests]
x:1 [in Top.Translation]
x:1 [in Top.TestEqualityEnv]
x:13 [in Top.RuleTests]
X:16 [in Top.Helpers]
X:28 [in Top.RuleTests]
x:3 [in Top.Translation]
X:40 [in Top.RuleTests]
X:62 [in Top.Helpers]
X:65 [in Top.Helpers]
x:8 [in Top.Translation]
X:9 [in Top.RuleTests]

Y

Y:10 [in Top.RuleTests]
Y:17 [in Top.Helpers]
y:2 [in Top.TestEqualityEnv]
Y:29 [in Top.RuleTests]
Y:41 [in Top.RuleTests]
Y:63 [in Top.Helpers]
Y:66 [in Top.Helpers]

Module Index

S

Source [in Top.Predefs]
SourceAnnot [in Top.Predefs]

T

Target [in Top.Predefs]

Library Index

H

Helpers

L

Library

P

Predefs

R

RuleTests

T

TestEquality
TestEqualityEnv
TestEquality3
TestHelpers
Translation

Lemma Index

C

construct_tuple_lemma [in Top.TestEquality3]

E

env_types [in Top.TestEqualityEnv]
eq_exfalso [in Top.Helpers]
eq_and_bot_exfalso [in Top.Helpers]
eq_and_self [in Top.Helpers]
eq_and_top [in Top.Helpers]
eq_and_bot [in Top.Helpers]
eq_and_merge [in Top.Helpers]
eq_and_comm [in Top.Helpers]
eq_and_assoc [in Top.Helpers]
eq_sel [in Top.Helpers]
eq_reflexive [in Top.Helpers]
eq_symmetry [in Top.Helpers]
eq_transitive [in Top.Helpers]

I

intersection_order [in Top.Helpers]

L

libTypes [in Top.Library]

N

neq_lib_env [in Top.Library]

O

obj_only_eq_and_rule_would_be_unsound [in Top.RuleTests]

P

p_transitivity_types [in Top.TestEquality]
p_coerce_types [in Top.TestEquality]
p_construct_types [in Top.TestEquality3]

S

simple_eq_and_rule_would_be_unsound [in Top.RuleTests]
sub_exfalso [in Top.Helpers]
sub_and_merge [in Top.Helpers]
sub_and_comm [in Top.Helpers]
sub_and_assoc2 [in Top.Helpers]
sub_and_assoc [in Top.Helpers]
swap_typ [in Top.Helpers]

W

weak_uniqueness_eq_and_rule_would_be_unsound [in Top.RuleTests]

Constructor Index

O

only_and [in Top.RuleTests]
only_typ [in Top.RuleTests]
only_val [in Top.RuleTests]
only_top [in Top.RuleTests]

T

typed_target_term_cons [in Top.Predefs]

Axiom Index

A

A [in Top.TestEquality]
Ai [in Top.Library]
AiAi [in Top.TestEqualityEnv]
AiBi [in Top.TestEqualityEnv]

B

B [in Top.TestEquality]
Bi [in Top.Library]
BiBi [in Top.TestEqualityEnv]

C

C [in Top.TestEquality]

D

data [in Top.Library]
diff [in Top.Library]

F

fst_v [in Top.Library]

G

GC [in Top.Library]
GenT [in Top.Library]
GN [in Top.Library]
gngc_simple [in Top.TestEqualityEnv]

M

mkTuple [in Top.Library]
mkUnit [in Top.Library]

P

pmatch [in Top.Library]
pmatch_data [in Top.TestEqualityEnv]

R

refl [in Top.TestEqualityEnv]

S

snd_v [in Top.Library]
snglhelper [in Top.TestEqualityEnv]

T

Tuple [in Top.Library]
T1 [in Top.Library]
T2 [in Top.Library]

U

Unit [in Top.Library]

Inductive Index

H

has_only_objects_or_top [in Top.RuleTests]

T

typed_target_term [in Top.Predefs]

Section Index

T

TestApp [in Top.TestEquality]

Definition Index

A

a [in Top.TestEquality]

B

b [in Top.TestEquality]

C

c [in Top.TestEquality]

E

empty_map [in Top.Translation]
env [in Top.Library]
envHlp [in Top.Library]
env_trm [in Top.TestEqualityEnv]
env_typ [in Top.TestEqualityEnv]
env_pretyp [in Top.TestEqualityEnv]

G

GenArgT [in Top.Library]
get_term [in Top.Predefs]

I

internalTupleTyp [in Top.Library]

L

lib [in Top.Library]
libInternalType [in Top.Library]
libPreType [in Top.Library]
libPreTypeHelp [in Top.Library]
libTrm [in Top.Library]
libType [in Top.Library]
lift_rec_defrhs [in Top.TestHelpers]
lift_rec_defs [in Top.TestHelpers]
lift_rec_def [in Top.TestHelpers]
lift_rec_val [in Top.TestHelpers]
lift_rec_trm [in Top.TestHelpers]
lift_rec_dec [in Top.TestHelpers]
lift_rec_typ [in Top.TestHelpers]
lift_rec_path [in Top.TestHelpers]
lift_rec_avar [in Top.TestHelpers]

M

make_fun_apply [in Top.TestHelpers]

O

open1 [in Top.Translation]

P

p_transitivity_trm [in Top.TestEquality]
p_transitivity_typ [in Top.TestEquality]
p_coerce_trm [in Top.TestEquality]
p_coerce_typ [in Top.TestEquality]
p_construct_trm [in Top.TestEquality3]
p_construct_typ [in Top.TestEquality3]

R

ref [in Top.Library]

S

shift1_p [in Top.TestHelpers]
shift1_trm [in Top.TestHelpers]
shift1_typ [in Top.TestHelpers]
skip1 [in Top.Translation]
sub [in Top.TestEquality]

T

t [in Top.TestEquality]
TLgen [in Top.TestHelpers]
translateType [in Top.Translation]
translateTyp0 [in Top.Translation]
TupleT [in Top.Library]
tupleTyp [in Top.Library]
type_map [in Top.Translation]

U

Unnamed_thm2 [in Top.TestEquality]
Unnamed_thm1 [in Top.TestEquality]
Unnamed_thm0 [in Top.TestEquality]
Unnamed_thm [in Top.TestEquality]

Global Index

other

(327 entries)

Notation Index

other

(5 entries)

Binder Index

other

(195 entries)

Module Index

other

(3 entries)

Library Index

other

(9 entries)

Lemma Index

other

(29 entries)

Constructor Index

other

(5 entries)

Axiom Index

other

(26 entries)

Inductive Index

other

(2 entries)

Section Index

other

(1 entry)

Definition Index

other

(52 entries)