| 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 | (516 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 | (13 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 | (332 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 | (6 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 | (30 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 | (46 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 | (19 entries) |
| 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 | (70 entries) |
Global Index
A
A:16 [binder, in TAL.Maps]A:17 [binder, in TAL.Maps]
A:19 [binder, in TAL.Maps]
A:24 [binder, in TAL.Maps]
A:27 [binder, in TAL.Maps]
A:31 [binder, in TAL.Maps]
A:36 [binder, in TAL.Maps]
A:41 [binder, in TAL.Maps]
A:44 [binder, in TAL.Maps]
A:50 [binder, in TAL.Maps]
A:51 [binder, in TAL.Maps]
A:52 [binder, in TAL.Maps]
A:56 [binder, in TAL.Maps]
A:58 [binder, in TAL.Maps]
A:62 [binder, in TAL.Maps]
A:67 [binder, in TAL.Maps]
A:72 [binder, in TAL.Maps]
A:76 [binder, in TAL.Maps]
B
beq_ty_map [definition, in TAL.TAL0.TypeSyntax]beq_ty [definition, in TAL.TAL0.TypeSyntax]
beq_idP [lemma, in TAL.Maps]
beq_id_false_iff [lemma, in TAL.Maps]
beq_id_true_iff [lemma, in TAL.Maps]
beq_id_refl [lemma, in TAL.Maps]
beq_id [definition, in TAL.Maps]
C
cc_operands_lbl [lemma, in TAL.TAL0.TypeSystem]cc_operands_int [lemma, in TAL.TAL0.TypeSystem]
cc_values_lbl [lemma, in TAL.TAL0.TypeSystem]
cc_values_int [lemma, in TAL.TAL0.TypeSystem]
ctx [inductive, in TAL.TAL0.TypeSystem]
ctx:114 [binder, in TAL.TAL0.TypeSystem]
ctx:115 [binder, in TAL.TAL0.TypeSystem]
c:109 [binder, in TAL.TAL0.TypeSystem]
c:116 [binder, in TAL.TAL0.TypeSystem]
c:122 [binder, in TAL.TAL0.TypeSystem]
c:81 [binder, in TAL.TAL0.TypeSystem]
c:85 [binder, in TAL.TAL0.TypeSystem]
D
d:20 [binder, in TAL.TAL0.Eval]d:27 [binder, in TAL.TAL0.Eval]
d:32 [binder, in TAL.TAL0.TypeSystem]
d:38 [binder, in TAL.TAL0.TypeSystem]
E
EmptyCtx [constructor, in TAL.TAL0.TypeSystem]empty_ty_map [definition, in TAL.TAL0.TypeSyntax]
empty_heap [definition, in TAL.TAL0.Syntax]
empty_regs [definition, in TAL.TAL0.Syntax]
ESFail [constructor, in TAL.TAL0.Eval]
ESSucc [constructor, in TAL.TAL0.Eval]
ESTrans [constructor, in TAL.TAL0.Eval]
Eval [library]
Examples [library]
exec_status [inductive, in TAL.TAL0.Eval]
ex_ftv_null_gamma [definition, in TAL.TAL0.Examples]
ex_ftv_null_b_gamma [definition, in TAL.TAL0.Examples]
ex_mstate_type_check_b [definition, in TAL.TAL0.Examples]
ex_heap_type_check_b [definition, in TAL.TAL0.Examples]
ex_regs_type_check_b [definition, in TAL.TAL0.Examples]
ex_loop_type_check_b [definition, in TAL.TAL0.Examples]
ex_loop_type_check [definition, in TAL.TAL0.Examples]
ex_mseval_prop_jump_to_loop [definition, in TAL.TAL0.Examples]
ex_mseval_res [definition, in TAL.TAL0.Examples]
ex_mseval_succ [definition, in TAL.TAL0.Examples]
ex_update_3 [definition, in TAL.Maps]
ex_update_2 [definition, in TAL.Maps]
ex_update_1 [definition, in TAL.Maps]
ex_update_0 [definition, in TAL.Maps]
ex_bool_map [definition, in TAL.Maps]
F
false_beq_id [lemma, in TAL.Maps]ftv_null_b [definition, in TAL.TAL0.TypeSyntax]
FTV_ForAll [constructor, in TAL.TAL0.TypeSyntax]
FTV_Code [constructor, in TAL.TAL0.TypeSyntax]
FTV_Int [constructor, in TAL.TAL0.TypeSyntax]
ftv_null [inductive, in TAL.TAL0.TypeSyntax]
G
gamma [definition, in TAL.TAL0.Examples]gamma_reg_4 [definition, in TAL.TAL0.Examples]
H
heap [definition, in TAL.TAL0.Syntax]heap_typed [definition, in TAL.TAL0.TypeSystem]
heap_has_type [inductive, in TAL.TAL0.TypeSystem]
H:11 [binder, in TAL.TAL0.Eval]
H:133 [binder, in TAL.TAL0.TypeSystem]
H:16 [binder, in TAL.TAL0.Eval]
H:170 [binder, in TAL.TAL0.TypeSystem]
H:176 [binder, in TAL.TAL0.TypeSystem]
H:181 [binder, in TAL.TAL0.TypeSystem]
H:187 [binder, in TAL.TAL0.TypeSystem]
H:193 [binder, in TAL.TAL0.TypeSystem]
H:2 [binder, in TAL.TAL0.Examples]
H:23 [binder, in TAL.TAL0.Eval]
H:32 [binder, in TAL.TAL0.Eval]
H:39 [binder, in TAL.TAL0.Eval]
H:70 [binder, in TAL.TAL0.TypeSystem]
H:78 [binder, in TAL.TAL0.TypeSystem]
I
IAdd [constructor, in TAL.TAL0.Syntax]Id [constructor, in TAL.Maps]
id [inductive, in TAL.Maps]
IJIf [constructor, in TAL.TAL0.Syntax]
IJmp [constructor, in TAL.TAL0.Syntax]
IMov [constructor, in TAL.TAL0.Syntax]
init_mstate [definition, in TAL.TAL0.Examples]
init_regs [definition, in TAL.TAL0.Examples]
init_heap [definition, in TAL.TAL0.Examples]
instr [inductive, in TAL.TAL0.Syntax]
instr_seq_type [definition, in TAL.TAL0.TypeSystem]
instr_type [definition, in TAL.TAL0.TypeSystem]
instr_seq_has_type [inductive, in TAL.TAL0.TypeSystem]
instr_has_type [inductive, in TAL.TAL0.TypeSystem]
instr_seq [inductive, in TAL.TAL0.Syntax]
ISeq [constructor, in TAL.TAL0.Syntax]
iseq_done [definition, in TAL.TAL0.Examples]
iseq_loop [definition, in TAL.TAL0.Examples]
iseq_prod [definition, in TAL.TAL0.Examples]
I':35 [binder, in TAL.TAL0.Eval]
i:10 [binder, in TAL.Maps]
I:118 [binder, in TAL.TAL0.TypeSystem]
i:12 [binder, in TAL.Maps]
I:13 [binder, in TAL.TAL0.Eval]
i:14 [binder, in TAL.Maps]
I:157 [binder, in TAL.TAL0.TypeSystem]
I:184 [binder, in TAL.TAL0.TypeSystem]
I:19 [binder, in TAL.TAL0.Eval]
I:197 [binder, in TAL.TAL0.TypeSystem]
i:21 [binder, in TAL.Maps]
i:25 [binder, in TAL.Maps]
I:26 [binder, in TAL.TAL0.Eval]
i:29 [binder, in TAL.Maps]
i:3 [binder, in TAL.Maps]
i:33 [binder, in TAL.Maps]
I:34 [binder, in TAL.TAL0.Eval]
i:38 [binder, in TAL.Maps]
I:41 [binder, in TAL.TAL0.Eval]
i:43 [binder, in TAL.Maps]
i:46 [binder, in TAL.Maps]
I:54 [binder, in TAL.TAL0.TypeSystem]
i:54 [binder, in TAL.Maps]
I:56 [binder, in TAL.TAL0.TypeSystem]
i:57 [binder, in TAL.Maps]
i:60 [binder, in TAL.Maps]
i:64 [binder, in TAL.Maps]
i:69 [binder, in TAL.Maps]
i:7 [binder, in TAL.Maps]
I:72 [binder, in TAL.TAL0.TypeSystem]
i:74 [binder, in TAL.Maps]
i:78 [binder, in TAL.Maps]
i:8 [binder, in TAL.Maps]
I:80 [binder, in TAL.TAL0.TypeSystem]
J
j:11 [binder, in TAL.Maps]j:13 [binder, in TAL.Maps]
j:15 [binder, in TAL.Maps]
j:23 [binder, in TAL.Maps]
j:34 [binder, in TAL.Maps]
j:4 [binder, in TAL.Maps]
j:47 [binder, in TAL.Maps]
j:65 [binder, in TAL.Maps]
j:79 [binder, in TAL.Maps]
j:9 [binder, in TAL.Maps]
L
lbl_exit [definition, in TAL.TAL0.Examples]lbl_done [definition, in TAL.TAL0.Examples]
lbl_loop [definition, in TAL.TAL0.Examples]
lbl_prod [definition, in TAL.TAL0.Examples]
l:15 [binder, in TAL.TAL0.Eval]
l:183 [binder, in TAL.TAL0.TypeSystem]
l:196 [binder, in TAL.TAL0.TypeSystem]
l:38 [binder, in TAL.TAL0.Eval]
l:57 [binder, in TAL.TAL0.TypeSyntax]
l:71 [binder, in TAL.TAL0.TypeSystem]
l:8 [binder, in TAL.TAL0.TypeSystem]
M
Maps [library]mseval [definition, in TAL.TAL0.Eval]
mseval_faithful [lemma, in TAL.TAL0.Eval]
mseval_prop_n [inductive, in TAL.TAL0.Eval]
mseval_prop [inductive, in TAL.TAL0.Eval]
mseval_n [definition, in TAL.TAL0.Eval]
MSt [constructor, in TAL.TAL0.Syntax]
mstate [inductive, in TAL.TAL0.Syntax]
mstate_ok_b [definition, in TAL.TAL0.TypeSystem]
mstate_ok [inductive, in TAL.TAL0.TypeSystem]
ms'':51 [binder, in TAL.TAL0.Eval]
ms':199 [binder, in TAL.TAL0.TypeSystem]
ms':48 [binder, in TAL.TAL0.Eval]
ms':50 [binder, in TAL.TAL0.Eval]
ms':53 [binder, in TAL.TAL0.Eval]
ms:137 [binder, in TAL.TAL0.TypeSystem]
ms:198 [binder, in TAL.TAL0.TypeSystem]
ms:3 [binder, in TAL.TAL0.Eval]
ms:47 [binder, in TAL.TAL0.Eval]
ms:49 [binder, in TAL.TAL0.Eval]
ms:52 [binder, in TAL.TAL0.Eval]
ms:6 [binder, in TAL.TAL0.Eval]
m:20 [binder, in TAL.Maps]
m:28 [binder, in TAL.Maps]
m:32 [binder, in TAL.Maps]
m:37 [binder, in TAL.Maps]
m:42 [binder, in TAL.Maps]
m:45 [binder, in TAL.Maps]
m:53 [binder, in TAL.Maps]
m:59 [binder, in TAL.Maps]
m:63 [binder, in TAL.Maps]
m:68 [binder, in TAL.Maps]
m:73 [binder, in TAL.Maps]
m:77 [binder, in TAL.Maps]
N
n1:30 [binder, in TAL.TAL0.Eval]n2:31 [binder, in TAL.TAL0.Eval]
n:178 [binder, in TAL.TAL0.TypeSystem]
n:190 [binder, in TAL.TAL0.TypeSystem]
n:5 [binder, in TAL.TAL0.Eval]
n:6 [binder, in TAL.TAL0.TypeSystem]
n:66 [binder, in TAL.TAL0.TypeSyntax]
P
partial_map [definition, in TAL.Maps]psi [definition, in TAL.TAL0.Examples]
PsiCtx [constructor, in TAL.TAL0.TypeSystem]
PsiGammaCtx [constructor, in TAL.TAL0.TypeSystem]
ps:15 [binder, in TAL.TAL0.TypeSyntax]
p_update_permute [lemma, in TAL.Maps]
p_update_same [lemma, in TAL.Maps]
p_update_shadow [lemma, in TAL.Maps]
p_update_neq [lemma, in TAL.Maps]
p_update_eq [lemma, in TAL.Maps]
p_apply_empty [lemma, in TAL.Maps]
p_update [definition, in TAL.Maps]
p_empty [definition, in TAL.Maps]
p:1 [binder, in TAL.TAL0.Examples]
p:126 [binder, in TAL.TAL0.TypeSystem]
p:134 [binder, in TAL.TAL0.TypeSystem]
p:16 [binder, in TAL.TAL0.TypeSyntax]
p:3 [binder, in TAL.TAL0.Examples]
p:49 [binder, in TAL.TAL0.TypeSyntax]
p:53 [binder, in TAL.TAL0.TypeSyntax]
p:65 [binder, in TAL.TAL0.TypeSyntax]
R
regs [definition, in TAL.TAL0.Syntax]regs_subst [lemma, in TAL.TAL0.TypeSystem]
regs_typed [definition, in TAL.TAL0.TypeSystem]
regs_has_type [inductive, in TAL.TAL0.TypeSystem]
reg_val [inductive, in TAL.TAL0.Syntax]
reg_4 [definition, in TAL.TAL0.Examples]
reg_3 [definition, in TAL.TAL0.Examples]
reg_2 [definition, in TAL.TAL0.Examples]
reg_1 [definition, in TAL.TAL0.Examples]
replace_ty_map [definition, in TAL.TAL0.TypeSyntax]
replace_ty [definition, in TAL.TAL0.TypeSyntax]
reval [definition, in TAL.TAL0.Syntax]
RLbl [constructor, in TAL.TAL0.Syntax]
RNum [constructor, in TAL.TAL0.Syntax]
R_Seq2 [constructor, in TAL.TAL0.Eval]
R_Seq1 [constructor, in TAL.TAL0.Eval]
R_If_Neq [constructor, in TAL.TAL0.Eval]
R_If_Eq [constructor, in TAL.TAL0.Eval]
R_Add [constructor, in TAL.TAL0.Eval]
R_Mov [constructor, in TAL.TAL0.Eval]
R_Jump [constructor, in TAL.TAL0.Eval]
R':18 [binder, in TAL.TAL0.Eval]
R':25 [binder, in TAL.TAL0.Eval]
R:12 [binder, in TAL.TAL0.Eval]
R:124 [binder, in TAL.TAL0.TypeSystem]
r:14 [binder, in TAL.TAL0.TypeSystem]
R:14 [binder, in TAL.TAL0.Syntax]
R:165 [binder, in TAL.TAL0.TypeSystem]
R:17 [binder, in TAL.TAL0.Eval]
R:171 [binder, in TAL.TAL0.TypeSystem]
R:188 [binder, in TAL.TAL0.TypeSystem]
R:194 [binder, in TAL.TAL0.TypeSystem]
R:24 [binder, in TAL.TAL0.Eval]
R:33 [binder, in TAL.TAL0.Eval]
r:36 [binder, in TAL.TAL0.Eval]
R:4 [binder, in TAL.TAL0.Examples]
R:40 [binder, in TAL.TAL0.Eval]
r:42 [binder, in TAL.TAL0.Eval]
r:43 [binder, in TAL.TAL0.TypeSystem]
R:63 [binder, in TAL.TAL0.TypeSystem]
r:64 [binder, in TAL.TAL0.TypeSystem]
R:79 [binder, in TAL.TAL0.TypeSystem]
S
soundness [lemma, in TAL.TAL0.TypeSystem]Syntax [library]
S_Mach [constructor, in TAL.TAL0.TypeSystem]
S_Heap [constructor, in TAL.TAL0.TypeSystem]
S_Regfile [constructor, in TAL.TAL0.TypeSystem]
S_Gen [constructor, in TAL.TAL0.TypeSystem]
S_Seq [constructor, in TAL.TAL0.TypeSystem]
S_Jump [constructor, in TAL.TAL0.TypeSystem]
S_If [constructor, in TAL.TAL0.TypeSystem]
S_Add [constructor, in TAL.TAL0.TypeSystem]
S_Mov [constructor, in TAL.TAL0.TypeSystem]
S_Inst [constructor, in TAL.TAL0.TypeSystem]
S_Val [constructor, in TAL.TAL0.TypeSystem]
S_Reg [constructor, in TAL.TAL0.TypeSystem]
S_Lab [constructor, in TAL.TAL0.TypeSystem]
S_Int [constructor, in TAL.TAL0.TypeSystem]
s:28 [binder, in TAL.TAL0.Eval]
s:39 [binder, in TAL.TAL0.TypeSystem]
T
TAlpha [constructor, in TAL.TAL0.TypeSyntax]TCode [constructor, in TAL.TAL0.TypeSyntax]
TForAll [constructor, in TAL.TAL0.TypeSyntax]
TInt [constructor, in TAL.TAL0.TypeSyntax]
tm':17 [binder, in TAL.TAL0.TypeSyntax]
tm:14 [binder, in TAL.TAL0.TypeSyntax]
tm:18 [binder, in TAL.TAL0.TypeSyntax]
tm:21 [binder, in TAL.TAL0.TypeSyntax]
tm:25 [binder, in TAL.TAL0.TypeSyntax]
tm:3 [binder, in TAL.TAL0.TypeSyntax]
tm:50 [binder, in TAL.TAL0.TypeSyntax]
tm:7 [binder, in TAL.TAL0.TypeSyntax]
tm:9 [binder, in TAL.TAL0.TypeSyntax]
total_map [definition, in TAL.Maps]
to_val [definition, in TAL.TAL0.Syntax]
tvs:61 [binder, in TAL.TAL0.TypeSyntax]
ty [inductive, in TAL.TAL0.TypeSyntax]
TypeSyntax [library]
TypeSystem [library]
ty_subst_regs [lemma, in TAL.TAL0.TypeSystem]
ty_subst_instr_seq [lemma, in TAL.TAL0.TypeSystem]
ty_subst_instr [lemma, in TAL.TAL0.TypeSystem]
ty_subst_val [lemma, in TAL.TAL0.TypeSystem]
ty_gen [definition, in TAL.TAL0.TypeSystem]
ty_inst [definition, in TAL.TAL0.TypeSystem]
ty_remove_quantifier [definition, in TAL.TAL0.TypeSystem]
ty_var_subst [definition, in TAL.TAL0.TypeSystem]
ty_remove [definition, in TAL.TAL0.TypeSyntax]
ty_update_neq [lemma, in TAL.TAL0.TypeSyntax]
ty_update_eq [lemma, in TAL.TAL0.TypeSyntax]
ty_update_list [definition, in TAL.TAL0.TypeSyntax]
ty_update [definition, in TAL.TAL0.TypeSyntax]
ty_lookup_int [definition, in TAL.TAL0.TypeSyntax]
ty_lookup [definition, in TAL.TAL0.TypeSyntax]
ty_map [definition, in TAL.TAL0.TypeSyntax]
t_update_permute [lemma, in TAL.Maps]
t_update_same [lemma, in TAL.Maps]
t_update_shadow [lemma, in TAL.Maps]
t_update_neq [lemma, in TAL.Maps]
t_update_eq [lemma, in TAL.Maps]
t_apply_empty [lemma, in TAL.Maps]
t_update [definition, in TAL.Maps]
t_empty [definition, in TAL.Maps]
t:62 [binder, in TAL.TAL0.TypeSyntax]
V
val [inductive, in TAL.TAL0.Syntax]value_type [definition, in TAL.TAL0.TypeSystem]
value_has_type [inductive, in TAL.TAL0.TypeSystem]
val_type [definition, in TAL.TAL0.TypeSystem]
val_has_type [inductive, in TAL.TAL0.TypeSystem]
VLbl [constructor, in TAL.TAL0.Syntax]
VNum [constructor, in TAL.TAL0.Syntax]
VReg [constructor, in TAL.TAL0.Syntax]
v':173 [binder, in TAL.TAL0.TypeSystem]
v1:39 [binder, in TAL.Maps]
v1:48 [binder, in TAL.Maps]
v1:70 [binder, in TAL.Maps]
v1:80 [binder, in TAL.Maps]
v2:40 [binder, in TAL.Maps]
v2:49 [binder, in TAL.Maps]
v2:71 [binder, in TAL.Maps]
v2:81 [binder, in TAL.Maps]
v:13 [binder, in TAL.TAL0.Syntax]
v:14 [binder, in TAL.TAL0.Eval]
v:144 [binder, in TAL.TAL0.TypeSystem]
v:172 [binder, in TAL.TAL0.TypeSystem]
v:177 [binder, in TAL.TAL0.TypeSystem]
v:18 [binder, in TAL.TAL0.TypeSystem]
v:18 [binder, in TAL.Maps]
v:182 [binder, in TAL.TAL0.TypeSystem]
v:189 [binder, in TAL.TAL0.TypeSystem]
v:195 [binder, in TAL.TAL0.TypeSystem]
v:21 [binder, in TAL.TAL0.Eval]
v:22 [binder, in TAL.TAL0.TypeSystem]
v:22 [binder, in TAL.Maps]
v:26 [binder, in TAL.Maps]
v:29 [binder, in TAL.TAL0.Eval]
v:30 [binder, in TAL.Maps]
v:33 [binder, in TAL.TAL0.TypeSystem]
v:35 [binder, in TAL.Maps]
v:37 [binder, in TAL.TAL0.Eval]
v:40 [binder, in TAL.TAL0.TypeSystem]
v:43 [binder, in TAL.TAL0.Eval]
v:44 [binder, in TAL.TAL0.TypeSystem]
v:49 [binder, in TAL.TAL0.TypeSystem]
v:55 [binder, in TAL.Maps]
v:61 [binder, in TAL.Maps]
v:65 [binder, in TAL.TAL0.TypeSystem]
v:66 [binder, in TAL.Maps]
v:75 [binder, in TAL.Maps]
v:82 [binder, in TAL.TAL0.TypeSystem]
v:86 [binder, in TAL.TAL0.TypeSystem]
W
w:11 [binder, in TAL.TAL0.Syntax]w:22 [binder, in TAL.TAL0.Eval]
X
xs:34 [binder, in TAL.TAL0.TypeSyntax]xs:39 [binder, in TAL.TAL0.TypeSyntax]
xs:95 [binder, in TAL.TAL0.TypeSystem]
x:10 [binder, in TAL.TAL0.TypeSyntax]
x:19 [binder, in TAL.TAL0.TypeSyntax]
x:22 [binder, in TAL.TAL0.TypeSyntax]
x:26 [binder, in TAL.TAL0.TypeSyntax]
x:4 [binder, in TAL.TAL0.TypeSyntax]
x:44 [binder, in TAL.TAL0.Eval]
x:8 [binder, in TAL.TAL0.TypeSyntax]
Y
ys:35 [binder, in TAL.TAL0.TypeSyntax]ys:40 [binder, in TAL.TAL0.TypeSyntax]
ys:96 [binder, in TAL.TAL0.TypeSystem]
y:23 [binder, in TAL.TAL0.TypeSyntax]
other
_ ;; _ [notation, in TAL.TAL0.Syntax]code( _ ) [notation, in TAL.TAL0.TypeSyntax]
int [notation, in TAL.TAL0.TypeSyntax]
JIF R( _ ) R( _ ) [notation, in TAL.TAL0.Syntax]
JIF R( _ ) _ [notation, in TAL.TAL0.Syntax]
JMP R( _ ) [notation, in TAL.TAL0.Syntax]
JMP _ [notation, in TAL.TAL0.Syntax]
R( _ ) +:= R( _ ) [notation, in TAL.TAL0.Syntax]
R( _ ) +:= _ [notation, in TAL.TAL0.Syntax]
R( _ ) := R( _ ) + R( _ ) [notation, in TAL.TAL0.Syntax]
R( _ ) := R( _ ) + _ [notation, in TAL.TAL0.Syntax]
R( _ ) := _ [notation, in TAL.TAL0.Syntax]
∀ _ .> _ [notation, in TAL.TAL0.TypeSyntax]
Γ':142 [binder, in TAL.TAL0.TypeSystem]
Γ':164 [binder, in TAL.TAL0.TypeSystem]
Γ':31 [binder, in TAL.TAL0.TypeSystem]
Γ':37 [binder, in TAL.TAL0.TypeSystem]
Γ1':150 [binder, in TAL.TAL0.TypeSystem]
Γ1:149 [binder, in TAL.TAL0.TypeSystem]
Γ2':152 [binder, in TAL.TAL0.TypeSystem]
Γ2:151 [binder, in TAL.TAL0.TypeSystem]
Γ2:52 [binder, in TAL.TAL0.TypeSystem]
Γ:110 [binder, in TAL.TAL0.TypeSystem]
Γ:117 [binder, in TAL.TAL0.TypeSystem]
Γ:123 [binder, in TAL.TAL0.TypeSystem]
Γ:13 [binder, in TAL.TAL0.TypeSystem]
Γ:132 [binder, in TAL.TAL0.TypeSystem]
Γ:136 [binder, in TAL.TAL0.TypeSystem]
Γ:141 [binder, in TAL.TAL0.TypeSystem]
Γ:163 [binder, in TAL.TAL0.TypeSystem]
Γ:169 [binder, in TAL.TAL0.TypeSystem]
Γ:17 [binder, in TAL.TAL0.TypeSystem]
Γ:180 [binder, in TAL.TAL0.TypeSystem]
Γ:186 [binder, in TAL.TAL0.TypeSystem]
Γ:192 [binder, in TAL.TAL0.TypeSystem]
Γ:21 [binder, in TAL.TAL0.TypeSystem]
Γ:30 [binder, in TAL.TAL0.TypeSystem]
Γ:36 [binder, in TAL.TAL0.TypeSystem]
Γ:42 [binder, in TAL.TAL0.TypeSystem]
Γ:48 [binder, in TAL.TAL0.TypeSystem]
Γ:51 [binder, in TAL.TAL0.TypeSystem]
Γ:56 [binder, in TAL.TAL0.TypeSyntax]
Γ:62 [binder, in TAL.TAL0.TypeSystem]
Γ:77 [binder, in TAL.TAL0.TypeSystem]
Ψ':140 [binder, in TAL.TAL0.TypeSystem]
Ψ:12 [binder, in TAL.TAL0.TypeSystem]
Ψ:131 [binder, in TAL.TAL0.TypeSystem]
Ψ:135 [binder, in TAL.TAL0.TypeSystem]
Ψ:139 [binder, in TAL.TAL0.TypeSystem]
Ψ:148 [binder, in TAL.TAL0.TypeSystem]
Ψ:156 [binder, in TAL.TAL0.TypeSystem]
Ψ:16 [binder, in TAL.TAL0.TypeSystem]
Ψ:162 [binder, in TAL.TAL0.TypeSystem]
Ψ:168 [binder, in TAL.TAL0.TypeSystem]
Ψ:175 [binder, in TAL.TAL0.TypeSystem]
Ψ:179 [binder, in TAL.TAL0.TypeSystem]
Ψ:185 [binder, in TAL.TAL0.TypeSystem]
Ψ:191 [binder, in TAL.TAL0.TypeSystem]
Ψ:20 [binder, in TAL.TAL0.TypeSystem]
Ψ:29 [binder, in TAL.TAL0.TypeSystem]
Ψ:35 [binder, in TAL.TAL0.TypeSystem]
Ψ:41 [binder, in TAL.TAL0.TypeSystem]
Ψ:47 [binder, in TAL.TAL0.TypeSystem]
Ψ:5 [binder, in TAL.TAL0.TypeSystem]
Ψ:50 [binder, in TAL.TAL0.TypeSystem]
Ψ:55 [binder, in TAL.TAL0.TypeSystem]
Ψ:61 [binder, in TAL.TAL0.TypeSystem]
Ψ:69 [binder, in TAL.TAL0.TypeSystem]
Ψ:7 [binder, in TAL.TAL0.TypeSystem]
Ψ:76 [binder, in TAL.TAL0.TypeSystem]
α:143 [binder, in TAL.TAL0.TypeSystem]
α:153 [binder, in TAL.TAL0.TypeSystem]
α:158 [binder, in TAL.TAL0.TypeSystem]
α:166 [binder, in TAL.TAL0.TypeSystem]
α:26 [binder, in TAL.TAL0.TypeSystem]
α:45 [binder, in TAL.TAL0.TypeSyntax]
α:51 [binder, in TAL.TAL0.TypeSyntax]
α:57 [binder, in TAL.TAL0.TypeSystem]
α:58 [binder, in TAL.TAL0.TypeSyntax]
α:91 [binder, in TAL.TAL0.TypeSystem]
ι:111 [binder, in TAL.TAL0.TypeSystem]
ι:154 [binder, in TAL.TAL0.TypeSystem]
ι:53 [binder, in TAL.TAL0.TypeSystem]
τ'':147 [binder, in TAL.TAL0.TypeSystem]
τ'':161 [binder, in TAL.TAL0.TypeSystem]
τ'':25 [binder, in TAL.TAL0.TypeSystem]
τ':103 [binder, in TAL.TAL0.TypeSystem]
τ':128 [binder, in TAL.TAL0.TypeSystem]
τ':146 [binder, in TAL.TAL0.TypeSystem]
τ':160 [binder, in TAL.TAL0.TypeSystem]
τ':24 [binder, in TAL.TAL0.TypeSystem]
τ':30 [binder, in TAL.TAL0.TypeSyntax]
τ':46 [binder, in TAL.TAL0.TypeSyntax]
τ':90 [binder, in TAL.TAL0.TypeSystem]
τ1:104 [binder, in TAL.TAL0.TypeSystem]
τ2':108 [binder, in TAL.TAL0.TypeSystem]
τ2:105 [binder, in TAL.TAL0.TypeSystem]
τ:100 [binder, in TAL.TAL0.TypeSystem]
τ:102 [binder, in TAL.TAL0.TypeSystem]
τ:11 [binder, in TAL.TAL0.TypeSyntax]
τ:127 [binder, in TAL.TAL0.TypeSystem]
τ:145 [binder, in TAL.TAL0.TypeSystem]
τ:15 [binder, in TAL.TAL0.TypeSystem]
τ:155 [binder, in TAL.TAL0.TypeSystem]
τ:159 [binder, in TAL.TAL0.TypeSystem]
τ:167 [binder, in TAL.TAL0.TypeSystem]
τ:174 [binder, in TAL.TAL0.TypeSystem]
τ:19 [binder, in TAL.TAL0.TypeSystem]
τ:20 [binder, in TAL.TAL0.TypeSyntax]
τ:23 [binder, in TAL.TAL0.TypeSystem]
τ:24 [binder, in TAL.TAL0.TypeSyntax]
τ:29 [binder, in TAL.TAL0.TypeSyntax]
τ:34 [binder, in TAL.TAL0.TypeSystem]
τ:44 [binder, in TAL.TAL0.TypeSyntax]
τ:52 [binder, in TAL.TAL0.TypeSyntax]
τ:58 [binder, in TAL.TAL0.TypeSystem]
τ:59 [binder, in TAL.TAL0.TypeSyntax]
τ:60 [binder, in TAL.TAL0.TypeSyntax]
τ:66 [binder, in TAL.TAL0.TypeSystem]
τ:73 [binder, in TAL.TAL0.TypeSystem]
τ:89 [binder, in TAL.TAL0.TypeSystem]
τ:9 [binder, in TAL.TAL0.TypeSystem]
Notation Index
other
_ ;; _ [in TAL.TAL0.Syntax]code( _ ) [in TAL.TAL0.TypeSyntax]
int [in TAL.TAL0.TypeSyntax]
JIF R( _ ) R( _ ) [in TAL.TAL0.Syntax]
JIF R( _ ) _ [in TAL.TAL0.Syntax]
JMP R( _ ) [in TAL.TAL0.Syntax]
JMP _ [in TAL.TAL0.Syntax]
R( _ ) +:= R( _ ) [in TAL.TAL0.Syntax]
R( _ ) +:= _ [in TAL.TAL0.Syntax]
R( _ ) := R( _ ) + R( _ ) [in TAL.TAL0.Syntax]
R( _ ) := R( _ ) + _ [in TAL.TAL0.Syntax]
R( _ ) := _ [in TAL.TAL0.Syntax]
∀ _ .> _ [in TAL.TAL0.TypeSyntax]
Binder Index
A
A:16 [in TAL.Maps]A:17 [in TAL.Maps]
A:19 [in TAL.Maps]
A:24 [in TAL.Maps]
A:27 [in TAL.Maps]
A:31 [in TAL.Maps]
A:36 [in TAL.Maps]
A:41 [in TAL.Maps]
A:44 [in TAL.Maps]
A:50 [in TAL.Maps]
A:51 [in TAL.Maps]
A:52 [in TAL.Maps]
A:56 [in TAL.Maps]
A:58 [in TAL.Maps]
A:62 [in TAL.Maps]
A:67 [in TAL.Maps]
A:72 [in TAL.Maps]
A:76 [in TAL.Maps]
C
ctx:114 [in TAL.TAL0.TypeSystem]ctx:115 [in TAL.TAL0.TypeSystem]
c:109 [in TAL.TAL0.TypeSystem]
c:116 [in TAL.TAL0.TypeSystem]
c:122 [in TAL.TAL0.TypeSystem]
c:81 [in TAL.TAL0.TypeSystem]
c:85 [in TAL.TAL0.TypeSystem]
D
d:20 [in TAL.TAL0.Eval]d:27 [in TAL.TAL0.Eval]
d:32 [in TAL.TAL0.TypeSystem]
d:38 [in TAL.TAL0.TypeSystem]
H
H:11 [in TAL.TAL0.Eval]H:133 [in TAL.TAL0.TypeSystem]
H:16 [in TAL.TAL0.Eval]
H:170 [in TAL.TAL0.TypeSystem]
H:176 [in TAL.TAL0.TypeSystem]
H:181 [in TAL.TAL0.TypeSystem]
H:187 [in TAL.TAL0.TypeSystem]
H:193 [in TAL.TAL0.TypeSystem]
H:2 [in TAL.TAL0.Examples]
H:23 [in TAL.TAL0.Eval]
H:32 [in TAL.TAL0.Eval]
H:39 [in TAL.TAL0.Eval]
H:70 [in TAL.TAL0.TypeSystem]
H:78 [in TAL.TAL0.TypeSystem]
I
I':35 [in TAL.TAL0.Eval]i:10 [in TAL.Maps]
I:118 [in TAL.TAL0.TypeSystem]
i:12 [in TAL.Maps]
I:13 [in TAL.TAL0.Eval]
i:14 [in TAL.Maps]
I:157 [in TAL.TAL0.TypeSystem]
I:184 [in TAL.TAL0.TypeSystem]
I:19 [in TAL.TAL0.Eval]
I:197 [in TAL.TAL0.TypeSystem]
i:21 [in TAL.Maps]
i:25 [in TAL.Maps]
I:26 [in TAL.TAL0.Eval]
i:29 [in TAL.Maps]
i:3 [in TAL.Maps]
i:33 [in TAL.Maps]
I:34 [in TAL.TAL0.Eval]
i:38 [in TAL.Maps]
I:41 [in TAL.TAL0.Eval]
i:43 [in TAL.Maps]
i:46 [in TAL.Maps]
I:54 [in TAL.TAL0.TypeSystem]
i:54 [in TAL.Maps]
I:56 [in TAL.TAL0.TypeSystem]
i:57 [in TAL.Maps]
i:60 [in TAL.Maps]
i:64 [in TAL.Maps]
i:69 [in TAL.Maps]
i:7 [in TAL.Maps]
I:72 [in TAL.TAL0.TypeSystem]
i:74 [in TAL.Maps]
i:78 [in TAL.Maps]
i:8 [in TAL.Maps]
I:80 [in TAL.TAL0.TypeSystem]
J
j:11 [in TAL.Maps]j:13 [in TAL.Maps]
j:15 [in TAL.Maps]
j:23 [in TAL.Maps]
j:34 [in TAL.Maps]
j:4 [in TAL.Maps]
j:47 [in TAL.Maps]
j:65 [in TAL.Maps]
j:79 [in TAL.Maps]
j:9 [in TAL.Maps]
L
l:15 [in TAL.TAL0.Eval]l:183 [in TAL.TAL0.TypeSystem]
l:196 [in TAL.TAL0.TypeSystem]
l:38 [in TAL.TAL0.Eval]
l:57 [in TAL.TAL0.TypeSyntax]
l:71 [in TAL.TAL0.TypeSystem]
l:8 [in TAL.TAL0.TypeSystem]
M
ms'':51 [in TAL.TAL0.Eval]ms':199 [in TAL.TAL0.TypeSystem]
ms':48 [in TAL.TAL0.Eval]
ms':50 [in TAL.TAL0.Eval]
ms':53 [in TAL.TAL0.Eval]
ms:137 [in TAL.TAL0.TypeSystem]
ms:198 [in TAL.TAL0.TypeSystem]
ms:3 [in TAL.TAL0.Eval]
ms:47 [in TAL.TAL0.Eval]
ms:49 [in TAL.TAL0.Eval]
ms:52 [in TAL.TAL0.Eval]
ms:6 [in TAL.TAL0.Eval]
m:20 [in TAL.Maps]
m:28 [in TAL.Maps]
m:32 [in TAL.Maps]
m:37 [in TAL.Maps]
m:42 [in TAL.Maps]
m:45 [in TAL.Maps]
m:53 [in TAL.Maps]
m:59 [in TAL.Maps]
m:63 [in TAL.Maps]
m:68 [in TAL.Maps]
m:73 [in TAL.Maps]
m:77 [in TAL.Maps]
N
n1:30 [in TAL.TAL0.Eval]n2:31 [in TAL.TAL0.Eval]
n:178 [in TAL.TAL0.TypeSystem]
n:190 [in TAL.TAL0.TypeSystem]
n:5 [in TAL.TAL0.Eval]
n:6 [in TAL.TAL0.TypeSystem]
n:66 [in TAL.TAL0.TypeSyntax]
P
ps:15 [in TAL.TAL0.TypeSyntax]p:1 [in TAL.TAL0.Examples]
p:126 [in TAL.TAL0.TypeSystem]
p:134 [in TAL.TAL0.TypeSystem]
p:16 [in TAL.TAL0.TypeSyntax]
p:3 [in TAL.TAL0.Examples]
p:49 [in TAL.TAL0.TypeSyntax]
p:53 [in TAL.TAL0.TypeSyntax]
p:65 [in TAL.TAL0.TypeSyntax]
R
R':18 [in TAL.TAL0.Eval]R':25 [in TAL.TAL0.Eval]
R:12 [in TAL.TAL0.Eval]
R:124 [in TAL.TAL0.TypeSystem]
r:14 [in TAL.TAL0.TypeSystem]
R:14 [in TAL.TAL0.Syntax]
R:165 [in TAL.TAL0.TypeSystem]
R:17 [in TAL.TAL0.Eval]
R:171 [in TAL.TAL0.TypeSystem]
R:188 [in TAL.TAL0.TypeSystem]
R:194 [in TAL.TAL0.TypeSystem]
R:24 [in TAL.TAL0.Eval]
R:33 [in TAL.TAL0.Eval]
r:36 [in TAL.TAL0.Eval]
R:4 [in TAL.TAL0.Examples]
R:40 [in TAL.TAL0.Eval]
r:42 [in TAL.TAL0.Eval]
r:43 [in TAL.TAL0.TypeSystem]
R:63 [in TAL.TAL0.TypeSystem]
r:64 [in TAL.TAL0.TypeSystem]
R:79 [in TAL.TAL0.TypeSystem]
S
s:28 [in TAL.TAL0.Eval]s:39 [in TAL.TAL0.TypeSystem]
T
tm':17 [in TAL.TAL0.TypeSyntax]tm:14 [in TAL.TAL0.TypeSyntax]
tm:18 [in TAL.TAL0.TypeSyntax]
tm:21 [in TAL.TAL0.TypeSyntax]
tm:25 [in TAL.TAL0.TypeSyntax]
tm:3 [in TAL.TAL0.TypeSyntax]
tm:50 [in TAL.TAL0.TypeSyntax]
tm:7 [in TAL.TAL0.TypeSyntax]
tm:9 [in TAL.TAL0.TypeSyntax]
tvs:61 [in TAL.TAL0.TypeSyntax]
t:62 [in TAL.TAL0.TypeSyntax]
V
v':173 [in TAL.TAL0.TypeSystem]v1:39 [in TAL.Maps]
v1:48 [in TAL.Maps]
v1:70 [in TAL.Maps]
v1:80 [in TAL.Maps]
v2:40 [in TAL.Maps]
v2:49 [in TAL.Maps]
v2:71 [in TAL.Maps]
v2:81 [in TAL.Maps]
v:13 [in TAL.TAL0.Syntax]
v:14 [in TAL.TAL0.Eval]
v:144 [in TAL.TAL0.TypeSystem]
v:172 [in TAL.TAL0.TypeSystem]
v:177 [in TAL.TAL0.TypeSystem]
v:18 [in TAL.TAL0.TypeSystem]
v:18 [in TAL.Maps]
v:182 [in TAL.TAL0.TypeSystem]
v:189 [in TAL.TAL0.TypeSystem]
v:195 [in TAL.TAL0.TypeSystem]
v:21 [in TAL.TAL0.Eval]
v:22 [in TAL.TAL0.TypeSystem]
v:22 [in TAL.Maps]
v:26 [in TAL.Maps]
v:29 [in TAL.TAL0.Eval]
v:30 [in TAL.Maps]
v:33 [in TAL.TAL0.TypeSystem]
v:35 [in TAL.Maps]
v:37 [in TAL.TAL0.Eval]
v:40 [in TAL.TAL0.TypeSystem]
v:43 [in TAL.TAL0.Eval]
v:44 [in TAL.TAL0.TypeSystem]
v:49 [in TAL.TAL0.TypeSystem]
v:55 [in TAL.Maps]
v:61 [in TAL.Maps]
v:65 [in TAL.TAL0.TypeSystem]
v:66 [in TAL.Maps]
v:75 [in TAL.Maps]
v:82 [in TAL.TAL0.TypeSystem]
v:86 [in TAL.TAL0.TypeSystem]
W
w:11 [in TAL.TAL0.Syntax]w:22 [in TAL.TAL0.Eval]
X
xs:34 [in TAL.TAL0.TypeSyntax]xs:39 [in TAL.TAL0.TypeSyntax]
xs:95 [in TAL.TAL0.TypeSystem]
x:10 [in TAL.TAL0.TypeSyntax]
x:19 [in TAL.TAL0.TypeSyntax]
x:22 [in TAL.TAL0.TypeSyntax]
x:26 [in TAL.TAL0.TypeSyntax]
x:4 [in TAL.TAL0.TypeSyntax]
x:44 [in TAL.TAL0.Eval]
x:8 [in TAL.TAL0.TypeSyntax]
Y
ys:35 [in TAL.TAL0.TypeSyntax]ys:40 [in TAL.TAL0.TypeSyntax]
ys:96 [in TAL.TAL0.TypeSystem]
y:23 [in TAL.TAL0.TypeSyntax]
other
Γ':142 [in TAL.TAL0.TypeSystem]Γ':164 [in TAL.TAL0.TypeSystem]
Γ':31 [in TAL.TAL0.TypeSystem]
Γ':37 [in TAL.TAL0.TypeSystem]
Γ1':150 [in TAL.TAL0.TypeSystem]
Γ1:149 [in TAL.TAL0.TypeSystem]
Γ2':152 [in TAL.TAL0.TypeSystem]
Γ2:151 [in TAL.TAL0.TypeSystem]
Γ2:52 [in TAL.TAL0.TypeSystem]
Γ:110 [in TAL.TAL0.TypeSystem]
Γ:117 [in TAL.TAL0.TypeSystem]
Γ:123 [in TAL.TAL0.TypeSystem]
Γ:13 [in TAL.TAL0.TypeSystem]
Γ:132 [in TAL.TAL0.TypeSystem]
Γ:136 [in TAL.TAL0.TypeSystem]
Γ:141 [in TAL.TAL0.TypeSystem]
Γ:163 [in TAL.TAL0.TypeSystem]
Γ:169 [in TAL.TAL0.TypeSystem]
Γ:17 [in TAL.TAL0.TypeSystem]
Γ:180 [in TAL.TAL0.TypeSystem]
Γ:186 [in TAL.TAL0.TypeSystem]
Γ:192 [in TAL.TAL0.TypeSystem]
Γ:21 [in TAL.TAL0.TypeSystem]
Γ:30 [in TAL.TAL0.TypeSystem]
Γ:36 [in TAL.TAL0.TypeSystem]
Γ:42 [in TAL.TAL0.TypeSystem]
Γ:48 [in TAL.TAL0.TypeSystem]
Γ:51 [in TAL.TAL0.TypeSystem]
Γ:56 [in TAL.TAL0.TypeSyntax]
Γ:62 [in TAL.TAL0.TypeSystem]
Γ:77 [in TAL.TAL0.TypeSystem]
Ψ':140 [in TAL.TAL0.TypeSystem]
Ψ:12 [in TAL.TAL0.TypeSystem]
Ψ:131 [in TAL.TAL0.TypeSystem]
Ψ:135 [in TAL.TAL0.TypeSystem]
Ψ:139 [in TAL.TAL0.TypeSystem]
Ψ:148 [in TAL.TAL0.TypeSystem]
Ψ:156 [in TAL.TAL0.TypeSystem]
Ψ:16 [in TAL.TAL0.TypeSystem]
Ψ:162 [in TAL.TAL0.TypeSystem]
Ψ:168 [in TAL.TAL0.TypeSystem]
Ψ:175 [in TAL.TAL0.TypeSystem]
Ψ:179 [in TAL.TAL0.TypeSystem]
Ψ:185 [in TAL.TAL0.TypeSystem]
Ψ:191 [in TAL.TAL0.TypeSystem]
Ψ:20 [in TAL.TAL0.TypeSystem]
Ψ:29 [in TAL.TAL0.TypeSystem]
Ψ:35 [in TAL.TAL0.TypeSystem]
Ψ:41 [in TAL.TAL0.TypeSystem]
Ψ:47 [in TAL.TAL0.TypeSystem]
Ψ:5 [in TAL.TAL0.TypeSystem]
Ψ:50 [in TAL.TAL0.TypeSystem]
Ψ:55 [in TAL.TAL0.TypeSystem]
Ψ:61 [in TAL.TAL0.TypeSystem]
Ψ:69 [in TAL.TAL0.TypeSystem]
Ψ:7 [in TAL.TAL0.TypeSystem]
Ψ:76 [in TAL.TAL0.TypeSystem]
α:143 [in TAL.TAL0.TypeSystem]
α:153 [in TAL.TAL0.TypeSystem]
α:158 [in TAL.TAL0.TypeSystem]
α:166 [in TAL.TAL0.TypeSystem]
α:26 [in TAL.TAL0.TypeSystem]
α:45 [in TAL.TAL0.TypeSyntax]
α:51 [in TAL.TAL0.TypeSyntax]
α:57 [in TAL.TAL0.TypeSystem]
α:58 [in TAL.TAL0.TypeSyntax]
α:91 [in TAL.TAL0.TypeSystem]
ι:111 [in TAL.TAL0.TypeSystem]
ι:154 [in TAL.TAL0.TypeSystem]
ι:53 [in TAL.TAL0.TypeSystem]
τ'':147 [in TAL.TAL0.TypeSystem]
τ'':161 [in TAL.TAL0.TypeSystem]
τ'':25 [in TAL.TAL0.TypeSystem]
τ':103 [in TAL.TAL0.TypeSystem]
τ':128 [in TAL.TAL0.TypeSystem]
τ':146 [in TAL.TAL0.TypeSystem]
τ':160 [in TAL.TAL0.TypeSystem]
τ':24 [in TAL.TAL0.TypeSystem]
τ':30 [in TAL.TAL0.TypeSyntax]
τ':46 [in TAL.TAL0.TypeSyntax]
τ':90 [in TAL.TAL0.TypeSystem]
τ1:104 [in TAL.TAL0.TypeSystem]
τ2':108 [in TAL.TAL0.TypeSystem]
τ2:105 [in TAL.TAL0.TypeSystem]
τ:100 [in TAL.TAL0.TypeSystem]
τ:102 [in TAL.TAL0.TypeSystem]
τ:11 [in TAL.TAL0.TypeSyntax]
τ:127 [in TAL.TAL0.TypeSystem]
τ:145 [in TAL.TAL0.TypeSystem]
τ:15 [in TAL.TAL0.TypeSystem]
τ:155 [in TAL.TAL0.TypeSystem]
τ:159 [in TAL.TAL0.TypeSystem]
τ:167 [in TAL.TAL0.TypeSystem]
τ:174 [in TAL.TAL0.TypeSystem]
τ:19 [in TAL.TAL0.TypeSystem]
τ:20 [in TAL.TAL0.TypeSyntax]
τ:23 [in TAL.TAL0.TypeSystem]
τ:24 [in TAL.TAL0.TypeSyntax]
τ:29 [in TAL.TAL0.TypeSyntax]
τ:34 [in TAL.TAL0.TypeSystem]
τ:44 [in TAL.TAL0.TypeSyntax]
τ:52 [in TAL.TAL0.TypeSyntax]
τ:58 [in TAL.TAL0.TypeSystem]
τ:59 [in TAL.TAL0.TypeSyntax]
τ:60 [in TAL.TAL0.TypeSyntax]
τ:66 [in TAL.TAL0.TypeSystem]
τ:73 [in TAL.TAL0.TypeSystem]
τ:89 [in TAL.TAL0.TypeSystem]
τ:9 [in TAL.TAL0.TypeSystem]
Library Index
E
EvalExamples
M
MapsS
SyntaxT
TypeSyntaxTypeSystem
Lemma Index
B
beq_idP [in TAL.Maps]beq_id_false_iff [in TAL.Maps]
beq_id_true_iff [in TAL.Maps]
beq_id_refl [in TAL.Maps]
C
cc_operands_lbl [in TAL.TAL0.TypeSystem]cc_operands_int [in TAL.TAL0.TypeSystem]
cc_values_lbl [in TAL.TAL0.TypeSystem]
cc_values_int [in TAL.TAL0.TypeSystem]
F
false_beq_id [in TAL.Maps]M
mseval_faithful [in TAL.TAL0.Eval]P
p_update_permute [in TAL.Maps]p_update_same [in TAL.Maps]
p_update_shadow [in TAL.Maps]
p_update_neq [in TAL.Maps]
p_update_eq [in TAL.Maps]
p_apply_empty [in TAL.Maps]
R
regs_subst [in TAL.TAL0.TypeSystem]S
soundness [in TAL.TAL0.TypeSystem]T
ty_subst_regs [in TAL.TAL0.TypeSystem]ty_subst_instr_seq [in TAL.TAL0.TypeSystem]
ty_subst_instr [in TAL.TAL0.TypeSystem]
ty_subst_val [in TAL.TAL0.TypeSystem]
ty_update_neq [in TAL.TAL0.TypeSyntax]
ty_update_eq [in TAL.TAL0.TypeSyntax]
t_update_permute [in TAL.Maps]
t_update_same [in TAL.Maps]
t_update_shadow [in TAL.Maps]
t_update_neq [in TAL.Maps]
t_update_eq [in TAL.Maps]
t_apply_empty [in TAL.Maps]
Constructor Index
E
EmptyCtx [in TAL.TAL0.TypeSystem]ESFail [in TAL.TAL0.Eval]
ESSucc [in TAL.TAL0.Eval]
ESTrans [in TAL.TAL0.Eval]
F
FTV_ForAll [in TAL.TAL0.TypeSyntax]FTV_Code [in TAL.TAL0.TypeSyntax]
FTV_Int [in TAL.TAL0.TypeSyntax]
I
IAdd [in TAL.TAL0.Syntax]Id [in TAL.Maps]
IJIf [in TAL.TAL0.Syntax]
IJmp [in TAL.TAL0.Syntax]
IMov [in TAL.TAL0.Syntax]
ISeq [in TAL.TAL0.Syntax]
M
MSt [in TAL.TAL0.Syntax]P
PsiCtx [in TAL.TAL0.TypeSystem]PsiGammaCtx [in TAL.TAL0.TypeSystem]
R
RLbl [in TAL.TAL0.Syntax]RNum [in TAL.TAL0.Syntax]
R_Seq2 [in TAL.TAL0.Eval]
R_Seq1 [in TAL.TAL0.Eval]
R_If_Neq [in TAL.TAL0.Eval]
R_If_Eq [in TAL.TAL0.Eval]
R_Add [in TAL.TAL0.Eval]
R_Mov [in TAL.TAL0.Eval]
R_Jump [in TAL.TAL0.Eval]
S
S_Mach [in TAL.TAL0.TypeSystem]S_Heap [in TAL.TAL0.TypeSystem]
S_Regfile [in TAL.TAL0.TypeSystem]
S_Gen [in TAL.TAL0.TypeSystem]
S_Seq [in TAL.TAL0.TypeSystem]
S_Jump [in TAL.TAL0.TypeSystem]
S_If [in TAL.TAL0.TypeSystem]
S_Add [in TAL.TAL0.TypeSystem]
S_Mov [in TAL.TAL0.TypeSystem]
S_Inst [in TAL.TAL0.TypeSystem]
S_Val [in TAL.TAL0.TypeSystem]
S_Reg [in TAL.TAL0.TypeSystem]
S_Lab [in TAL.TAL0.TypeSystem]
S_Int [in TAL.TAL0.TypeSystem]
T
TAlpha [in TAL.TAL0.TypeSyntax]TCode [in TAL.TAL0.TypeSyntax]
TForAll [in TAL.TAL0.TypeSyntax]
TInt [in TAL.TAL0.TypeSyntax]
V
VLbl [in TAL.TAL0.Syntax]VNum [in TAL.TAL0.Syntax]
VReg [in TAL.TAL0.Syntax]
Inductive Index
C
ctx [in TAL.TAL0.TypeSystem]E
exec_status [in TAL.TAL0.Eval]F
ftv_null [in TAL.TAL0.TypeSyntax]H
heap_has_type [in TAL.TAL0.TypeSystem]I
id [in TAL.Maps]instr [in TAL.TAL0.Syntax]
instr_seq_has_type [in TAL.TAL0.TypeSystem]
instr_has_type [in TAL.TAL0.TypeSystem]
instr_seq [in TAL.TAL0.Syntax]
M
mseval_prop_n [in TAL.TAL0.Eval]mseval_prop [in TAL.TAL0.Eval]
mstate [in TAL.TAL0.Syntax]
mstate_ok [in TAL.TAL0.TypeSystem]
R
regs_has_type [in TAL.TAL0.TypeSystem]reg_val [in TAL.TAL0.Syntax]
T
ty [in TAL.TAL0.TypeSyntax]V
val [in TAL.TAL0.Syntax]value_has_type [in TAL.TAL0.TypeSystem]
val_has_type [in TAL.TAL0.TypeSystem]
Definition Index
B
beq_ty_map [in TAL.TAL0.TypeSyntax]beq_ty [in TAL.TAL0.TypeSyntax]
beq_id [in TAL.Maps]
E
empty_ty_map [in TAL.TAL0.TypeSyntax]empty_heap [in TAL.TAL0.Syntax]
empty_regs [in TAL.TAL0.Syntax]
ex_ftv_null_gamma [in TAL.TAL0.Examples]
ex_ftv_null_b_gamma [in TAL.TAL0.Examples]
ex_mstate_type_check_b [in TAL.TAL0.Examples]
ex_heap_type_check_b [in TAL.TAL0.Examples]
ex_regs_type_check_b [in TAL.TAL0.Examples]
ex_loop_type_check_b [in TAL.TAL0.Examples]
ex_loop_type_check [in TAL.TAL0.Examples]
ex_mseval_prop_jump_to_loop [in TAL.TAL0.Examples]
ex_mseval_res [in TAL.TAL0.Examples]
ex_mseval_succ [in TAL.TAL0.Examples]
ex_update_3 [in TAL.Maps]
ex_update_2 [in TAL.Maps]
ex_update_1 [in TAL.Maps]
ex_update_0 [in TAL.Maps]
ex_bool_map [in TAL.Maps]
F
ftv_null_b [in TAL.TAL0.TypeSyntax]G
gamma [in TAL.TAL0.Examples]gamma_reg_4 [in TAL.TAL0.Examples]
H
heap [in TAL.TAL0.Syntax]heap_typed [in TAL.TAL0.TypeSystem]
I
init_mstate [in TAL.TAL0.Examples]init_regs [in TAL.TAL0.Examples]
init_heap [in TAL.TAL0.Examples]
instr_seq_type [in TAL.TAL0.TypeSystem]
instr_type [in TAL.TAL0.TypeSystem]
iseq_done [in TAL.TAL0.Examples]
iseq_loop [in TAL.TAL0.Examples]
iseq_prod [in TAL.TAL0.Examples]
L
lbl_exit [in TAL.TAL0.Examples]lbl_done [in TAL.TAL0.Examples]
lbl_loop [in TAL.TAL0.Examples]
lbl_prod [in TAL.TAL0.Examples]
M
mseval [in TAL.TAL0.Eval]mseval_n [in TAL.TAL0.Eval]
mstate_ok_b [in TAL.TAL0.TypeSystem]
P
partial_map [in TAL.Maps]psi [in TAL.TAL0.Examples]
p_update [in TAL.Maps]
p_empty [in TAL.Maps]
R
regs [in TAL.TAL0.Syntax]regs_typed [in TAL.TAL0.TypeSystem]
reg_4 [in TAL.TAL0.Examples]
reg_3 [in TAL.TAL0.Examples]
reg_2 [in TAL.TAL0.Examples]
reg_1 [in TAL.TAL0.Examples]
replace_ty_map [in TAL.TAL0.TypeSyntax]
replace_ty [in TAL.TAL0.TypeSyntax]
reval [in TAL.TAL0.Syntax]
T
total_map [in TAL.Maps]to_val [in TAL.TAL0.Syntax]
ty_gen [in TAL.TAL0.TypeSystem]
ty_inst [in TAL.TAL0.TypeSystem]
ty_remove_quantifier [in TAL.TAL0.TypeSystem]
ty_var_subst [in TAL.TAL0.TypeSystem]
ty_remove [in TAL.TAL0.TypeSyntax]
ty_update_list [in TAL.TAL0.TypeSyntax]
ty_update [in TAL.TAL0.TypeSyntax]
ty_lookup_int [in TAL.TAL0.TypeSyntax]
ty_lookup [in TAL.TAL0.TypeSyntax]
ty_map [in TAL.TAL0.TypeSyntax]
t_update [in TAL.Maps]
t_empty [in TAL.Maps]
V
value_type [in TAL.TAL0.TypeSystem]val_type [in TAL.TAL0.TypeSystem]
| 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 | (516 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 | (13 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 | (332 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 | (6 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 | (30 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 | (46 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 | (19 entries) |
| 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 | (70 entries) |
This page has been generated by coqdoc