| Global Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (308 entries) |
| Notation Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (5 entries) |
| Binder Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (174 entries) |
| Module Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (3 entries) |
| Library Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (9 entries) |
| Lemma Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (29 entries) |
| Constructor Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (1 entry) |
| Axiom Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (26 entries) |
| Inductive Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (1 entry) |
| Section Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (1 entry) |
| Definition Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (59 entries) |
Global Index
A
A [axiom, in Top.TestEquality]a [definition, in Top.TestEquality]
acc:26 [binder, in Top.Translation]
Ai [axiom, in Top.Library]
AiAi [axiom, in Top.TestEqualityEnv]
AiBi [axiom, in Top.TestEqualityEnv]
arg:48 [binder, in Top.TestHelpers]
A1:2 [binder, in Top.Helpers]
A2:4 [binder, in Top.Helpers]
A:11 [binder, in Top.Helpers]
A:14 [binder, in Top.Helpers]
A:2 [binder, in Top.TestEquality3]
A:22 [binder, in Top.Helpers]
A:25 [binder, in Top.Helpers]
A:29 [binder, in Top.Helpers]
a:3 [binder, in Top.TestHelpers]
A:33 [binder, in Top.Helpers]
A:37 [binder, in Top.Helpers]
A:40 [binder, in Top.Helpers]
A:43 [binder, in Top.Helpers]
A:48 [binder, in Top.Helpers]
A:53 [binder, in Top.Helpers]
A:55 [binder, in Top.Helpers]
A:57 [binder, in Top.Helpers]
A:59 [binder, in Top.Helpers]
A:7 [binder, in Top.Helpers]
A:72 [binder, in Top.Helpers]
A:76 [binder, in Top.Helpers]
B
B [axiom, in Top.TestEquality]b [definition, in Top.TestEquality]
base:25 [binder, in Top.Translation]
Bi [axiom, in Top.Library]
BiBi [axiom, in Top.TestEqualityEnv]
B1:3 [binder, in Top.Helpers]
B2:5 [binder, in Top.Helpers]
B:12 [binder, in Top.Helpers]
B:26 [binder, in Top.Helpers]
B:3 [binder, in Top.TestEquality3]
B:30 [binder, in Top.Helpers]
B:34 [binder, in Top.Helpers]
B:38 [binder, in Top.Helpers]
B:41 [binder, in Top.Helpers]
B:44 [binder, in Top.Helpers]
B:49 [binder, in Top.Helpers]
B:60 [binder, in Top.Helpers]
B:8 [binder, in Top.Helpers]
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
empty_map [definition, in Top.Translation]env [definition, in Top.Library]
envHlp [definition, in Top.Library]
env_types [lemma, in Top.TestEqualityEnv]
env_trm [definition, in Top.TestEqualityEnv]
env_typ [definition, in Top.TestEqualityEnv]
env_pretyp [definition, in Top.TestEqualityEnv]
eq_inv_direct [lemma, in Top.Helpers]
eq_inv [lemma, in Top.Helpers]
eq_exfalso [lemma, in Top.Helpers]
eq_and_bot_exfalso [lemma, in Top.Helpers]
eq_and_self [lemma, in Top.Helpers]
eq_and_top [lemma, in Top.Helpers]
eq_and_bot [lemma, in Top.Helpers]
eq_and_merge [lemma, in Top.Helpers]
eq_and_comm [lemma, in Top.Helpers]
eq_and_assoc [lemma, in Top.Helpers]
eq_sel [lemma, in Top.Helpers]
eq_reflexive [lemma, in Top.Helpers]
eq_symmetry [lemma, in Top.Helpers]
eq_transitive [lemma, in Top.Helpers]
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.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.Library]
G:24 [binder, in Top.Helpers]
G:28 [binder, in Top.Helpers]
G:32 [binder, in Top.Helpers]
G:36 [binder, in Top.Helpers]
G:39 [binder, in Top.Helpers]
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:67 [binder, in Top.Helpers]
G:73 [binder, in Top.Helpers]
H
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]
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
main:39 [binder, in Top.Translation]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
offset:17 [binder, in Top.Library]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_destruct_types [lemma, in Top.TestEquality2]
p_destruct_trm [definition, in Top.TestEquality2]
p_destruct_typ [definition, in Top.TestEquality2]
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]
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]
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]
TestEquality2 [library]
TestEquality3 [library]
TestHelpers [library]
TLgen [definition, in Top.TestHelpers]
translateEnvTrm [definition, in Top.Translation]
translateEnvTypOpened [definition, in Top.Translation]
translateProgram [definition, in Top.Translation]
translateTerm [definition, in Top.Translation]
translateType [definition, in Top.Translation]
translateTyp0 [definition, in Top.Translation]
Translation [library]
trmenv:35 [binder, in Top.Translation]
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]
TypedTrm [definition, in Top.Translation]
typed_target_term_cons [constructor, in Top.Predefs]
typed_target_term [inductive, in Top.Predefs]
typenv:34 [binder, in Top.Translation]
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:22 [binder, in Top.Translation]
T1:70 [binder, in Top.Helpers]
T1:74 [binder, in Top.Helpers]
T2 [axiom, in Top.Library]
T2':19 [binder, in Top.Translation]
T2':21 [binder, in Top.Translation]
T2:71 [binder, in Top.Helpers]
T2:75 [binder, in Top.Helpers]
T:11 [binder, in Top.TestHelpers]
T:12 [binder, in Top.Translation]
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:27 [binder, in Top.Translation]
t:3 [binder, in Top.Predefs]
T:30 [binder, in Top.Translation]
t:36 [binder, in Top.Translation]
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: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:20 [binder, in Top.TestHelpers]
u:23 [binder, in Top.TestHelpers]
u:26 [binder, in Top.TestHelpers]
u:29 [binder, in Top.TestHelpers]
u:32 [binder, in Top.TestHelpers]
V
v:24 [binder, in Top.TestHelpers]W
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
X1:68 [binder, in Top.Helpers]X2:69 [binder, in Top.Helpers]
x:1 [binder, in Top.Translation]
x:1 [binder, in Top.TestEqualityEnv]
X:16 [binder, in Top.Helpers]
x:3 [binder, in Top.Translation]
X:62 [binder, in Top.Helpers]
X:65 [binder, in Top.Helpers]
x:8 [binder, in Top.Translation]
Y
Y:17 [binder, in Top.Helpers]y:2 [binder, in Top.TestEqualityEnv]
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]
Σ:31 [binder, in Top.Translation]
Σ:32 [binder, in Top.Translation]
Σ:33 [binder, in Top.Translation]
Σ:38 [binder, in Top.Translation]
Notation Index
other
_ ⊢ _ =:= _ [in Top.Helpers]_ $$ _ [in Top.TestHelpers]
_ $ _ [in Top.TestHelpers]
{ _ == _ } [in Top.Helpers]
{( _ , .. , _ )} [in Top.Helpers]
Binder Index
A
acc:26 [in Top.Translation]arg:48 [in Top.TestHelpers]
A1:2 [in Top.Helpers]
A2:4 [in Top.Helpers]
A:11 [in Top.Helpers]
A:14 [in Top.Helpers]
A:2 [in Top.TestEquality3]
A:22 [in Top.Helpers]
A:25 [in Top.Helpers]
A:29 [in Top.Helpers]
a:3 [in Top.TestHelpers]
A:33 [in Top.Helpers]
A:37 [in Top.Helpers]
A:40 [in Top.Helpers]
A:43 [in Top.Helpers]
A:48 [in Top.Helpers]
A:53 [in Top.Helpers]
A:55 [in Top.Helpers]
A:57 [in Top.Helpers]
A:59 [in Top.Helpers]
A:7 [in Top.Helpers]
A:72 [in Top.Helpers]
A:76 [in Top.Helpers]
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: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
G:1 [in Top.Helpers]G:1 [in Top.TestEquality3]
G:10 [in Top.Helpers]
G:13 [in Top.Helpers]
G:15 [in Top.Helpers]
G:20 [in Top.Helpers]
G:20 [in Top.Library]
G:24 [in Top.Helpers]
G:28 [in Top.Helpers]
G:32 [in Top.Helpers]
G:36 [in Top.Helpers]
G:39 [in Top.Helpers]
G:42 [in Top.Helpers]
G:47 [in Top.Helpers]
G:52 [in Top.Helpers]
G:54 [in Top.Helpers]
G:56 [in Top.Helpers]
G:58 [in Top.Helpers]
G:6 [in Top.Helpers]
G:61 [in Top.Helpers]
G:64 [in Top.Helpers]
G:67 [in Top.Helpers]
G:73 [in Top.Helpers]
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]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]
M
main:39 [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
trmenv:35 [in Top.Translation]Ts':24 [in Top.Translation]
TT1:21 [in Top.Library]
TT2:22 [in Top.Library]
typenv:34 [in Top.Translation]
ty_map:13 [in Top.Translation]
T1':18 [in Top.Translation]
T1':20 [in Top.Translation]
T1:22 [in Top.Translation]
T1:70 [in Top.Helpers]
T1:74 [in Top.Helpers]
T2':19 [in Top.Translation]
T2':21 [in Top.Translation]
T2:71 [in Top.Helpers]
T2:75 [in Top.Helpers]
T:11 [in Top.TestHelpers]
T:12 [in Top.Translation]
T:19 [in Top.Helpers]
t:21 [in Top.TestHelpers]
T:23 [in Top.Helpers]
t:23 [in Top.Translation]
T:27 [in Top.Translation]
t:3 [in Top.Predefs]
T:30 [in Top.Translation]
t:36 [in Top.Translation]
T:4 [in Top.Predefs]
t:4 [in Top.TestEquality]
t:44 [in Top.TestHelpers]
t:45 [in Top.TestHelpers]
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:20 [in Top.TestHelpers]
u:23 [in Top.TestHelpers]
u:26 [in Top.TestHelpers]
u:29 [in Top.TestHelpers]
u:32 [in Top.TestHelpers]
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:68 [in Top.Helpers]X2:69 [in Top.Helpers]
x:1 [in Top.Translation]
x:1 [in Top.TestEqualityEnv]
X:16 [in Top.Helpers]
x:3 [in Top.Translation]
X:62 [in Top.Helpers]
X:65 [in Top.Helpers]
x:8 [in Top.Translation]
Y
Y:17 [in Top.Helpers]y:2 [in Top.TestEqualityEnv]
Y:63 [in Top.Helpers]
Y:66 [in Top.Helpers]
other
Σ:31 [in Top.Translation]Σ:32 [in Top.Translation]
Σ:33 [in Top.Translation]
Σ:38 [in Top.Translation]
Module Index
S
Source [in Top.Predefs]SourceAnnot [in Top.Predefs]
T
Target [in Top.Predefs]Library Index
H
HelpersL
LibraryP
PredefsT
TestEqualityTestEqualityEnv
TestEquality2
TestEquality3
TestHelpers
Translation
Lemma Index
C
construct_tuple_lemma [in Top.TestEquality3]E
env_types [in Top.TestEqualityEnv]eq_inv_direct [in Top.Helpers]
eq_inv [in Top.Helpers]
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]P
p_transitivity_types [in Top.TestEquality]p_coerce_types [in Top.TestEquality]
p_construct_types [in Top.TestEquality3]
p_destruct_types [in Top.TestEquality2]
S
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]
Constructor Index
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
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]
p_destruct_trm [in Top.TestEquality2]
p_destruct_typ [in Top.TestEquality2]
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]
translateEnvTrm [in Top.Translation]
translateEnvTypOpened [in Top.Translation]
translateProgram [in Top.Translation]
translateTerm [in Top.Translation]
translateType [in Top.Translation]
translateTyp0 [in Top.Translation]
TupleT [in Top.Library]
tupleTyp [in Top.Library]
TypedTrm [in Top.Translation]
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 | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (308 entries) |
| Notation Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (5 entries) |
| Binder Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (174 entries) |
| Module Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (3 entries) |
| Library Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (9 entries) |
| Lemma Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (29 entries) |
| Constructor Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (1 entry) |
| Axiom Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (26 entries) |
| Inductive Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (1 entry) |
| Section Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (1 entry) |
| Definition Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (59 entries) |