| 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 | (729 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 | (6 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 | (459 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 | (4 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 | (12 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 | (49 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 | (118 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 | (25 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 | (56 entries) |
Global Index
A
Add [constructor, in PreTalent22.Spl_in_class]Add [constructor, in PreTalent22.Spl_completed]
Add [constructor, in PreTalent22.Spl]
addition_multiplication [module, in PreTalent22.Arith]
addition_multiplication.add [definition, in PreTalent22.Arith_in_class]
addition_multiplication [module, in PreTalent22.Arith_in_class]
Add_typed [constructor, in PreTalent22.Spl_completed]
add_assoc [lemma, in PreTalent22.Arith]
add_comm [lemma, in PreTalent22.Arith]
add_assoc [lemma, in PreTalent22.Arith_in_class]
add_comm [lemma, in PreTalent22.Arith_in_class]
add_S [lemma, in PreTalent22.Arith_in_class]
add_zero [lemma, in PreTalent22.Arith_in_class]
add23 [definition, in PreTalent22.SplVM]
add23 [definition, in PreTalent22.Spl_in_class]
add23 [definition, in PreTalent22.SplVM_in_class]
add23 [definition, in PreTalent22.Spl_completed]
add23 [definition, in PreTalent22.SplVM_before_third_session]
add23 [definition, in PreTalent22.Spl]
And [constructor, in PreTalent22.Spl_in_class]
And [constructor, in PreTalent22.Spl_completed]
And [constructor, in PreTalent22.Spl]
And_typed [constructor, in PreTalent22.Spl_completed]
Arith [library]
Arith_in_class [library]
A:11 [binder, in PreTalent22.SplVM]
A:11 [binder, in PreTalent22.SplVM_in_class]
A:11 [binder, in PreTalent22.SplVM_before_third_session]
a:13 [binder, in PreTalent22.SplVM]
a:13 [binder, in PreTalent22.SplVM_in_class]
a:13 [binder, in PreTalent22.SplVM_before_third_session]
A:5 [binder, in PreTalent22.SplVM]
A:5 [binder, in PreTalent22.SplVM_in_class]
A:5 [binder, in PreTalent22.SplVM_before_third_session]
a:7 [binder, in PreTalent22.SplVM]
a:7 [binder, in PreTalent22.SplVM_in_class]
a:7 [binder, in PreTalent22.SplVM_before_third_session]
B
bad_prog [definition, in PreTalent22.SplVM]bad_prog [definition, in PreTalent22.Spl_in_class]
bad_prog [definition, in PreTalent22.SplVM_in_class]
bad_prog [definition, in PreTalent22.Spl_completed]
bad_prog [definition, in PreTalent22.SplVM_before_third_session]
bad_prog [definition, in PreTalent22.Spl]
Bool [constructor, in PreTalent22.Spl_in_class]
Bool [constructor, in PreTalent22.Spl_completed]
Bool [constructor, in PreTalent22.Spl]
BoolEl [constructor, in PreTalent22.SplVM]
BoolEl [constructor, in PreTalent22.SplVM_in_class]
BoolEl [constructor, in PreTalent22.SplVM_before_third_session]
BoolRes [constructor, in PreTalent22.Spl_in_class]
BoolRes [constructor, in PreTalent22.Spl_completed]
BoolRes [constructor, in PreTalent22.Spl]
BoolRes_typed [constructor, in PreTalent22.Spl_in_class]
BoolRes_typed [constructor, in PreTalent22.Spl_completed]
Bool_typed [constructor, in PreTalent22.Spl_in_class]
Bool_typed [constructor, in PreTalent22.Spl_completed]
bool_res_rel [constructor, in PreTalent22.Compiler]
bool_res_rel [constructor, in PreTalent22.Compiler_in_class]
b1:30 [binder, in PreTalent22.SplVM_in_class]
b1:30 [binder, in PreTalent22.SplVM_before_third_session]
b1:34 [binder, in PreTalent22.SplVM_in_class]
b1:34 [binder, in PreTalent22.SplVM_before_third_session]
b1:55 [binder, in PreTalent22.Spl_in_class]
b1:55 [binder, in PreTalent22.Spl_completed]
b1:57 [binder, in PreTalent22.Spl_in_class]
b1:57 [binder, in PreTalent22.Spl_completed]
b2:28 [binder, in PreTalent22.SplVM_in_class]
b2:28 [binder, in PreTalent22.SplVM_before_third_session]
b2:32 [binder, in PreTalent22.SplVM_in_class]
b2:32 [binder, in PreTalent22.SplVM_before_third_session]
b2:56 [binder, in PreTalent22.Spl_in_class]
b2:56 [binder, in PreTalent22.Spl_completed]
b2:58 [binder, in PreTalent22.Spl_in_class]
b2:58 [binder, in PreTalent22.Spl_completed]
b:20 [binder, in PreTalent22.SplVM]
b:20 [binder, in PreTalent22.SplVM_in_class]
b:20 [binder, in PreTalent22.SplVM_before_third_session]
b:25 [binder, in PreTalent22.Compiler]
b:25 [binder, in PreTalent22.Compiler_in_class]
b:26 [binder, in PreTalent22.SplVM]
b:26 [binder, in PreTalent22.Spl_in_class]
b:26 [binder, in PreTalent22.SplVM_in_class]
b:26 [binder, in PreTalent22.Spl_completed]
b:26 [binder, in PreTalent22.SplVM_before_third_session]
b:26 [binder, in PreTalent22.Spl]
b:36 [binder, in PreTalent22.SplVM_in_class]
b:36 [binder, in PreTalent22.SplVM_before_third_session]
b:37 [binder, in PreTalent22.Spl_in_class]
b:37 [binder, in PreTalent22.Spl_completed]
b:37 [binder, in PreTalent22.Spl]
b:4 [binder, in PreTalent22.SplVM]
b:4 [binder, in PreTalent22.Spl_in_class]
b:4 [binder, in PreTalent22.SplVM_in_class]
b:4 [binder, in PreTalent22.Spl_completed]
b:4 [binder, in PreTalent22.SplVM_before_third_session]
b:4 [binder, in PreTalent22.Spl]
b:46 [binder, in PreTalent22.Spl_in_class]
b:46 [binder, in PreTalent22.Spl_completed]
b:46 [binder, in PreTalent22.Spl]
b:50 [binder, in PreTalent22.Spl_in_class]
b:50 [binder, in PreTalent22.Spl_completed]
b:50 [binder, in PreTalent22.Spl]
b:54 [binder, in PreTalent22.Spl_in_class]
b:54 [binder, in PreTalent22.Spl_completed]
b:54 [binder, in PreTalent22.Spl]
b:59 [binder, in PreTalent22.Spl_in_class]
b:59 [binder, in PreTalent22.Spl_completed]
b:75 [binder, in PreTalent22.Spl_in_class]
b:79 [binder, in PreTalent22.Spl_in_class]
b:79 [binder, in PreTalent22.Spl_completed]
C
CJump [constructor, in PreTalent22.SplVM]CJump [constructor, in PreTalent22.SplVM_in_class]
CJump [constructor, in PreTalent22.SplVM_before_third_session]
compile [definition, in PreTalent22.Compiler]
compile [definition, in PreTalent22.Compiler_in_class]
Compiler [library]
Compiler_in_class [library]
compile_correct [lemma, in PreTalent22.Compiler]
compile_correct [lemma, in PreTalent22.Compiler_in_class]
compile_correct_gen [lemma, in PreTalent22.Compiler_in_class]
Coq [library]
c:5 [binder, in PreTalent22.Spl_in_class]
c:5 [binder, in PreTalent22.Spl_completed]
c:5 [binder, in PreTalent22.Spl]
c:80 [binder, in PreTalent22.Spl_in_class]
c:80 [binder, in PreTalent22.Spl_completed]
D
DoAdd [constructor, in PreTalent22.SplVM]DoAdd [constructor, in PreTalent22.SplVM_in_class]
DoAdd [constructor, in PreTalent22.SplVM_before_third_session]
DoAnd [constructor, in PreTalent22.SplVM]
DoAnd [constructor, in PreTalent22.SplVM_in_class]
DoAnd [constructor, in PreTalent22.SplVM_before_third_session]
DoEq [constructor, in PreTalent22.SplVM]
DoEq [constructor, in PreTalent22.SplVM_in_class]
DoEq [constructor, in PreTalent22.SplVM_before_third_session]
DoLe [constructor, in PreTalent22.SplVM]
DoLe [constructor, in PreTalent22.SplVM_in_class]
DoLe [constructor, in PreTalent22.SplVM_before_third_session]
DoMul [constructor, in PreTalent22.SplVM]
DoMul [constructor, in PreTalent22.SplVM_in_class]
DoMul [constructor, in PreTalent22.SplVM_before_third_session]
DoNot [constructor, in PreTalent22.SplVM]
DoNot [constructor, in PreTalent22.SplVM_in_class]
DoNot [constructor, in PreTalent22.SplVM_before_third_session]
DoOr [constructor, in PreTalent22.SplVM]
DoOr [constructor, in PreTalent22.SplVM_in_class]
DoOr [constructor, in PreTalent22.SplVM_before_third_session]
DoSub [constructor, in PreTalent22.SplVM]
DoSub [constructor, in PreTalent22.SplVM_in_class]
DoSub [constructor, in PreTalent22.SplVM_before_third_session]
E
Eq [constructor, in PreTalent22.Spl_in_class]Eq [constructor, in PreTalent22.Spl_completed]
Eq [constructor, in PreTalent22.Spl]
Eq_typed [constructor, in PreTalent22.Spl_completed]
Err [constructor, in PreTalent22.Spl_in_class]
Err [constructor, in PreTalent22.Spl_completed]
Err [constructor, in PreTalent22.Spl]
eval [definition, in PreTalent22.Spl_in_class]
eval [definition, in PreTalent22.Spl_completed]
eval [definition, in PreTalent22.Spl]
eval_respects_types [lemma, in PreTalent22.Spl_in_class]
eval_respects_types [lemma, in PreTalent22.Spl_completed]
eval_respects_types [lemma, in PreTalent22.Spl]
expand_add_mul [lemma, in PreTalent22.Arith]
expand_add_mul [lemma, in PreTalent22.Arith_in_class]
expr [inductive, in PreTalent22.Spl_in_class]
expr [inductive, in PreTalent22.Spl_completed]
expr [inductive, in PreTalent22.Spl]
e1:10 [binder, in PreTalent22.Spl_in_class]
e1:10 [binder, in PreTalent22.Spl_completed]
e1:10 [binder, in PreTalent22.Spl]
e1:13 [binder, in PreTalent22.Spl_in_class]
e1:13 [binder, in PreTalent22.Spl_completed]
e1:13 [binder, in PreTalent22.Spl]
e1:15 [binder, in PreTalent22.Spl_in_class]
e1:15 [binder, in PreTalent22.Spl_completed]
e1:15 [binder, in PreTalent22.Spl]
e1:17 [binder, in PreTalent22.Spl_in_class]
e1:17 [binder, in PreTalent22.Spl_completed]
e1:17 [binder, in PreTalent22.Spl]
e1:19 [binder, in PreTalent22.Spl_in_class]
e1:19 [binder, in PreTalent22.Spl_completed]
e1:19 [binder, in PreTalent22.Spl]
e1:21 [binder, in PreTalent22.Spl_in_class]
e1:21 [binder, in PreTalent22.Spl_completed]
e1:21 [binder, in PreTalent22.Spl]
e1:8 [binder, in PreTalent22.Spl_in_class]
e1:8 [binder, in PreTalent22.Spl_completed]
e1:8 [binder, in PreTalent22.Spl]
e1:84 [binder, in PreTalent22.Spl_completed]
e1:86 [binder, in PreTalent22.Spl_completed]
e1:89 [binder, in PreTalent22.Spl_completed]
e1:91 [binder, in PreTalent22.Spl_completed]
e1:93 [binder, in PreTalent22.Spl_completed]
e1:95 [binder, in PreTalent22.Spl_completed]
e1:97 [binder, in PreTalent22.Spl_completed]
e2:11 [binder, in PreTalent22.Spl_in_class]
e2:11 [binder, in PreTalent22.Spl_completed]
e2:11 [binder, in PreTalent22.Spl]
e2:14 [binder, in PreTalent22.Spl_in_class]
e2:14 [binder, in PreTalent22.Spl_completed]
e2:14 [binder, in PreTalent22.Spl]
e2:16 [binder, in PreTalent22.Spl_in_class]
e2:16 [binder, in PreTalent22.Spl_completed]
e2:16 [binder, in PreTalent22.Spl]
e2:18 [binder, in PreTalent22.Spl_in_class]
e2:18 [binder, in PreTalent22.Spl_completed]
e2:18 [binder, in PreTalent22.Spl]
e2:20 [binder, in PreTalent22.Spl_in_class]
e2:20 [binder, in PreTalent22.Spl_completed]
e2:20 [binder, in PreTalent22.Spl]
e2:22 [binder, in PreTalent22.Spl_in_class]
e2:22 [binder, in PreTalent22.Spl_completed]
e2:22 [binder, in PreTalent22.Spl]
e2:85 [binder, in PreTalent22.Spl_completed]
e2:87 [binder, in PreTalent22.Spl_completed]
e2:9 [binder, in PreTalent22.Spl_in_class]
e2:9 [binder, in PreTalent22.Spl_completed]
e2:9 [binder, in PreTalent22.Spl]
e2:90 [binder, in PreTalent22.Spl_completed]
e2:92 [binder, in PreTalent22.Spl_completed]
e2:94 [binder, in PreTalent22.Spl_completed]
e2:96 [binder, in PreTalent22.Spl_completed]
e2:98 [binder, in PreTalent22.Spl_completed]
e:1 [binder, in PreTalent22.Compiler]
e:1 [binder, in PreTalent22.Compiler_in_class]
e:101 [binder, in PreTalent22.Spl_completed]
e:103 [binder, in PreTalent22.Spl_completed]
e:12 [binder, in PreTalent22.Spl_in_class]
e:12 [binder, in PreTalent22.Spl_completed]
e:12 [binder, in PreTalent22.Spl]
e:26 [binder, in PreTalent22.Compiler]
e:26 [binder, in PreTalent22.Compiler_in_class]
e:29 [binder, in PreTalent22.Compiler_in_class]
e:51 [binder, in PreTalent22.Spl_in_class]
e:51 [binder, in PreTalent22.Spl_completed]
e:51 [binder, in PreTalent22.Spl]
e:63 [binder, in PreTalent22.Spl]
e:65 [binder, in PreTalent22.Spl]
e:67 [binder, in PreTalent22.Spl]
e:84 [binder, in PreTalent22.Spl_in_class]
e:86 [binder, in PreTalent22.Spl_in_class]
e:88 [binder, in PreTalent22.Spl_in_class]
e:88 [binder, in PreTalent22.Spl_completed]
e:99 [binder, in PreTalent22.Spl_completed]
F
f:14 [binder, in PreTalent22.SplVM]f:14 [binder, in PreTalent22.SplVM_in_class]
f:14 [binder, in PreTalent22.SplVM_before_third_session]
f:28 [binder, in PreTalent22.Spl_in_class]
f:28 [binder, in PreTalent22.Spl_completed]
f:28 [binder, in PreTalent22.Spl]
f:31 [binder, in PreTalent22.Spl_in_class]
f:31 [binder, in PreTalent22.Spl_completed]
f:31 [binder, in PreTalent22.Spl]
f:33 [binder, in PreTalent22.Spl_in_class]
f:33 [binder, in PreTalent22.Spl_completed]
f:33 [binder, in PreTalent22.Spl]
f:36 [binder, in PreTalent22.Spl_in_class]
f:36 [binder, in PreTalent22.Spl_completed]
f:36 [binder, in PreTalent22.Spl]
f:40 [binder, in PreTalent22.Spl_in_class]
f:40 [binder, in PreTalent22.Spl_completed]
f:40 [binder, in PreTalent22.Spl]
f:43 [binder, in PreTalent22.Spl_in_class]
f:43 [binder, in PreTalent22.Spl_completed]
f:43 [binder, in PreTalent22.Spl]
f:45 [binder, in PreTalent22.Spl_in_class]
f:45 [binder, in PreTalent22.Spl_completed]
f:45 [binder, in PreTalent22.Spl]
f:48 [binder, in PreTalent22.Spl_in_class]
f:48 [binder, in PreTalent22.Spl_completed]
f:48 [binder, in PreTalent22.Spl]
f:7 [binder, in PreTalent22.Spl_in_class]
f:7 [binder, in PreTalent22.Spl_completed]
f:7 [binder, in PreTalent22.Spl]
f:8 [binder, in PreTalent22.SplVM]
f:8 [binder, in PreTalent22.SplVM_in_class]
f:8 [binder, in PreTalent22.SplVM_before_third_session]
f:82 [binder, in PreTalent22.Spl_in_class]
f:82 [binder, in PreTalent22.Spl_completed]
G
Gauss [lemma, in PreTalent22.Arith]Gauss [lemma, in PreTalent22.Arith_in_class]
I
if3le5 [definition, in PreTalent22.SplVM]if3le5 [definition, in PreTalent22.Spl_in_class]
if3le5 [definition, in PreTalent22.SplVM_in_class]
if3le5 [definition, in PreTalent22.Spl_completed]
if3le5 [definition, in PreTalent22.SplVM_before_third_session]
if3le5 [definition, in PreTalent22.Spl]
ITE [constructor, in PreTalent22.Spl_in_class]
ITE [constructor, in PreTalent22.Spl_completed]
ITE [constructor, in PreTalent22.Spl]
ITE_typed [constructor, in PreTalent22.Spl_in_class]
ITE_typed [constructor, in PreTalent22.Spl_completed]
i:24 [binder, in PreTalent22.SplVM]
i:24 [binder, in PreTalent22.SplVM_in_class]
i:24 [binder, in PreTalent22.SplVM_before_third_session]
J
Jump [constructor, in PreTalent22.SplVM]Jump [constructor, in PreTalent22.SplVM_in_class]
Jump [constructor, in PreTalent22.SplVM_before_third_session]
j:21 [binder, in PreTalent22.SplVM]
j:21 [binder, in PreTalent22.SplVM_in_class]
j:21 [binder, in PreTalent22.SplVM_before_third_session]
j:22 [binder, in PreTalent22.SplVM]
j:22 [binder, in PreTalent22.SplVM_in_class]
j:22 [binder, in PreTalent22.SplVM_before_third_session]
K
k:10 [binder, in PreTalent22.Arith]k:13 [binder, in PreTalent22.Arith]
k:17 [binder, in PreTalent22.Arith_in_class]
k:20 [binder, in PreTalent22.Arith_in_class]
L
Le [constructor, in PreTalent22.Spl_in_class]Le [constructor, in PreTalent22.Spl_completed]
Le [constructor, in PreTalent22.Spl]
Le_typed [constructor, in PreTalent22.Spl_completed]
l:14 [binder, in PreTalent22.Arith]
l:21 [binder, in PreTalent22.Arith_in_class]
M
Mul [constructor, in PreTalent22.Spl_in_class]Mul [constructor, in PreTalent22.Spl_completed]
Mul [constructor, in PreTalent22.Spl]
Mul_typed [constructor, in PreTalent22.Spl_completed]
m:12 [binder, in PreTalent22.Arith]
m:12 [binder, in PreTalent22.Arith_in_class]
m:14 [binder, in PreTalent22.Arith_in_class]
m:16 [binder, in PreTalent22.Arith_in_class]
m:19 [binder, in PreTalent22.Arith_in_class]
m:4 [binder, in PreTalent22.Arith_in_class]
m:7 [binder, in PreTalent22.Arith]
m:9 [binder, in PreTalent22.Arith]
N
Nat [module, in PreTalent22.Arith]Nat [module, in PreTalent22.Arith_in_class]
Nat.nat [inductive, in PreTalent22.Arith]
Nat.nat [inductive, in PreTalent22.Arith_in_class]
Nat.O [constructor, in PreTalent22.Arith]
Nat.O [constructor, in PreTalent22.Arith_in_class]
Nat.S [constructor, in PreTalent22.Arith]
Nat.S [constructor, in PreTalent22.Arith_in_class]
Not [constructor, in PreTalent22.Spl_in_class]
Not [constructor, in PreTalent22.Spl_completed]
Not [constructor, in PreTalent22.Spl]
Not_typed [constructor, in PreTalent22.Spl_completed]
Num [constructor, in PreTalent22.Spl_in_class]
Num [constructor, in PreTalent22.Spl_completed]
Num [constructor, in PreTalent22.Spl]
NumEl [constructor, in PreTalent22.SplVM]
NumEl [constructor, in PreTalent22.SplVM_in_class]
NumEl [constructor, in PreTalent22.SplVM_before_third_session]
NumRes [constructor, in PreTalent22.Spl_in_class]
NumRes [constructor, in PreTalent22.Spl_completed]
NumRes [constructor, in PreTalent22.Spl]
NumRes_typed [constructor, in PreTalent22.Spl_in_class]
NumRes_typed [constructor, in PreTalent22.Spl_completed]
NumRes_typed [constructor, in PreTalent22.Spl]
Num_typed [constructor, in PreTalent22.Spl_in_class]
Num_typed [constructor, in PreTalent22.Spl_completed]
num_res_rel [constructor, in PreTalent22.Compiler]
num_res_rel [constructor, in PreTalent22.Compiler_in_class]
Num_typed [constructor, in PreTalent22.Spl]
n1:40 [binder, in PreTalent22.SplVM_in_class]
n1:40 [binder, in PreTalent22.SplVM_before_third_session]
n1:44 [binder, in PreTalent22.SplVM_in_class]
n1:44 [binder, in PreTalent22.SplVM_before_third_session]
n1:48 [binder, in PreTalent22.SplVM_in_class]
n1:48 [binder, in PreTalent22.SplVM_before_third_session]
n1:52 [binder, in PreTalent22.SplVM_in_class]
n1:52 [binder, in PreTalent22.SplVM_before_third_session]
n1:56 [binder, in PreTalent22.SplVM_in_class]
n1:56 [binder, in PreTalent22.SplVM_before_third_session]
n1:60 [binder, in PreTalent22.Spl_in_class]
n1:60 [binder, in PreTalent22.Spl_completed]
n1:62 [binder, in PreTalent22.Spl_in_class]
n1:62 [binder, in PreTalent22.Spl_completed]
n1:64 [binder, in PreTalent22.Spl_in_class]
n1:64 [binder, in PreTalent22.Spl_completed]
n1:66 [binder, in PreTalent22.Spl_in_class]
n1:66 [binder, in PreTalent22.Spl_completed]
n1:68 [binder, in PreTalent22.Spl_in_class]
n1:68 [binder, in PreTalent22.Spl_completed]
n2:38 [binder, in PreTalent22.SplVM_in_class]
n2:38 [binder, in PreTalent22.SplVM_before_third_session]
n2:42 [binder, in PreTalent22.SplVM_in_class]
n2:42 [binder, in PreTalent22.SplVM_before_third_session]
n2:46 [binder, in PreTalent22.SplVM_in_class]
n2:46 [binder, in PreTalent22.SplVM_before_third_session]
n2:50 [binder, in PreTalent22.SplVM_in_class]
n2:50 [binder, in PreTalent22.SplVM_before_third_session]
n2:54 [binder, in PreTalent22.SplVM_in_class]
n2:54 [binder, in PreTalent22.SplVM_before_third_session]
n2:61 [binder, in PreTalent22.Spl_in_class]
n2:61 [binder, in PreTalent22.Spl_completed]
n2:63 [binder, in PreTalent22.Spl_in_class]
n2:63 [binder, in PreTalent22.Spl_completed]
n2:65 [binder, in PreTalent22.Spl_in_class]
n2:65 [binder, in PreTalent22.Spl_completed]
n2:67 [binder, in PreTalent22.Spl_in_class]
n2:67 [binder, in PreTalent22.Spl_completed]
n2:69 [binder, in PreTalent22.Spl_in_class]
n2:69 [binder, in PreTalent22.Spl_completed]
n:10 [binder, in PreTalent22.Arith_in_class]
n:11 [binder, in PreTalent22.Arith]
n:11 [binder, in PreTalent22.Arith_in_class]
n:13 [binder, in PreTalent22.Arith_in_class]
n:15 [binder, in PreTalent22.Arith]
n:15 [binder, in PreTalent22.Arith_in_class]
n:16 [binder, in PreTalent22.Arith]
n:18 [binder, in PreTalent22.Arith_in_class]
n:19 [binder, in PreTalent22.SplVM]
n:19 [binder, in PreTalent22.SplVM_in_class]
n:19 [binder, in PreTalent22.SplVM_before_third_session]
n:22 [binder, in PreTalent22.Arith_in_class]
n:23 [binder, in PreTalent22.Arith_in_class]
n:24 [binder, in PreTalent22.Compiler]
n:24 [binder, in PreTalent22.Compiler_in_class]
n:25 [binder, in PreTalent22.Spl_in_class]
n:25 [binder, in PreTalent22.Spl_completed]
n:25 [binder, in PreTalent22.Spl]
n:3 [binder, in PreTalent22.SplVM]
n:3 [binder, in PreTalent22.Spl_in_class]
n:3 [binder, in PreTalent22.SplVM_in_class]
n:3 [binder, in PreTalent22.Spl_completed]
n:3 [binder, in PreTalent22.SplVM_before_third_session]
n:3 [binder, in PreTalent22.Arith]
n:3 [binder, in PreTalent22.Arith_in_class]
n:3 [binder, in PreTalent22.Spl]
n:34 [binder, in PreTalent22.Spl_in_class]
n:34 [binder, in PreTalent22.Spl_completed]
n:34 [binder, in PreTalent22.Spl]
n:38 [binder, in PreTalent22.Spl_in_class]
n:38 [binder, in PreTalent22.Spl_completed]
n:38 [binder, in PreTalent22.Spl]
n:49 [binder, in PreTalent22.Spl_in_class]
n:49 [binder, in PreTalent22.Spl_completed]
n:49 [binder, in PreTalent22.Spl]
n:59 [binder, in PreTalent22.Spl]
n:6 [binder, in PreTalent22.Arith]
n:62 [binder, in PreTalent22.Spl]
n:7 [binder, in PreTalent22.Arith_in_class]
n:74 [binder, in PreTalent22.Spl_in_class]
n:74 [binder, in PreTalent22.Spl_completed]
n:75 [binder, in PreTalent22.Spl_completed]
n:78 [binder, in PreTalent22.Spl_in_class]
n:78 [binder, in PreTalent22.Spl_completed]
n:8 [binder, in PreTalent22.Arith]
O
Or [constructor, in PreTalent22.Spl_in_class]Or [constructor, in PreTalent22.Spl_completed]
Or [constructor, in PreTalent22.Spl]
Or_typed [constructor, in PreTalent22.Spl_completed]
Overture [library]
P
pop_bool [definition, in PreTalent22.SplVM]pop_num [definition, in PreTalent22.SplVM]
pop_bool [definition, in PreTalent22.SplVM_in_class]
pop_num [definition, in PreTalent22.SplVM_in_class]
pop_bool [definition, in PreTalent22.SplVM_before_third_session]
pop_num [definition, in PreTalent22.SplVM_before_third_session]
PushBool [constructor, in PreTalent22.SplVM]
PushBool [constructor, in PreTalent22.SplVM_in_class]
PushBool [constructor, in PreTalent22.SplVM_before_third_session]
PushNum [constructor, in PreTalent22.SplVM]
PushNum [constructor, in PreTalent22.SplVM_in_class]
PushNum [constructor, in PreTalent22.SplVM_before_third_session]
p1:38 [binder, in PreTalent22.SplVM]
p1:44 [binder, in PreTalent22.SplVM]
p1:68 [binder, in PreTalent22.SplVM_in_class]
p1:68 [binder, in PreTalent22.SplVM_before_third_session]
p1:74 [binder, in PreTalent22.SplVM_in_class]
p1:74 [binder, in PreTalent22.SplVM_before_third_session]
p2:39 [binder, in PreTalent22.SplVM]
p2:45 [binder, in PreTalent22.SplVM]
p2:69 [binder, in PreTalent22.SplVM_in_class]
p2:69 [binder, in PreTalent22.SplVM_before_third_session]
p2:75 [binder, in PreTalent22.SplVM_in_class]
p2:75 [binder, in PreTalent22.SplVM_before_third_session]
p:30 [binder, in PreTalent22.SplVM]
p:60 [binder, in PreTalent22.SplVM_in_class]
p:60 [binder, in PreTalent22.SplVM_before_third_session]
p:78 [binder, in PreTalent22.SplVM_in_class]
R
result [inductive, in PreTalent22.Spl_in_class]result [inductive, in PreTalent22.Spl_completed]
result [inductive, in PreTalent22.Spl]
result_rel [inductive, in PreTalent22.Compiler]
result_rel [inductive, in PreTalent22.Compiler_in_class]
res_typed [inductive, in PreTalent22.Spl_in_class]
res_typed [inductive, in PreTalent22.Spl_completed]
res_typed [inductive, in PreTalent22.Spl]
runVMInstr [definition, in PreTalent22.SplVM]
runVMInstr [definition, in PreTalent22.SplVM_in_class]
runVMInstr [definition, in PreTalent22.SplVM_before_third_session]
runVMProg [definition, in PreTalent22.SplVM]
runVMProg [definition, in PreTalent22.SplVM_in_class]
runVMProg [definition, in PreTalent22.SplVM_before_third_session]
runVMProg_jump [lemma, in PreTalent22.SplVM]
runVMProg_app [lemma, in PreTalent22.SplVM]
runVMProg_whole_jump [lemma, in PreTalent22.SplVM_in_class]
runVMProg_jump [lemma, in PreTalent22.SplVM_in_class]
runVMProg_app [lemma, in PreTalent22.SplVM_in_class]
runVMProg_jump [lemma, in PreTalent22.SplVM_before_third_session]
runVMProg_app [lemma, in PreTalent22.SplVM_before_third_session]
r:27 [binder, in PreTalent22.Spl_in_class]
r:27 [binder, in PreTalent22.Spl_completed]
r:27 [binder, in PreTalent22.Spl]
r:30 [binder, in PreTalent22.Spl_in_class]
r:30 [binder, in PreTalent22.Spl_completed]
r:30 [binder, in PreTalent22.Spl]
r:32 [binder, in PreTalent22.Spl_in_class]
r:32 [binder, in PreTalent22.Spl_completed]
r:32 [binder, in PreTalent22.Spl]
r:35 [binder, in PreTalent22.Spl_in_class]
r:35 [binder, in PreTalent22.Spl_completed]
r:35 [binder, in PreTalent22.Spl]
r:39 [binder, in PreTalent22.Spl_in_class]
r:39 [binder, in PreTalent22.Spl_completed]
r:39 [binder, in PreTalent22.Spl]
r:42 [binder, in PreTalent22.Spl_in_class]
r:42 [binder, in PreTalent22.Spl_completed]
r:42 [binder, in PreTalent22.Spl]
r:44 [binder, in PreTalent22.Spl_in_class]
r:44 [binder, in PreTalent22.Spl_completed]
r:44 [binder, in PreTalent22.Spl]
r:47 [binder, in PreTalent22.Spl_in_class]
r:47 [binder, in PreTalent22.Spl_completed]
r:47 [binder, in PreTalent22.Spl]
S
se:27 [binder, in PreTalent22.Compiler]se:28 [binder, in PreTalent22.Compiler_in_class]
se:30 [binder, in PreTalent22.Compiler_in_class]
skip':40 [binder, in PreTalent22.SplVM]
skip':70 [binder, in PreTalent22.SplVM_in_class]
skip':70 [binder, in PreTalent22.SplVM_before_third_session]
skip:29 [binder, in PreTalent22.SplVM]
skip:37 [binder, in PreTalent22.SplVM]
skip:43 [binder, in PreTalent22.SplVM]
skip:59 [binder, in PreTalent22.SplVM_in_class]
skip:59 [binder, in PreTalent22.SplVM_before_third_session]
skip:67 [binder, in PreTalent22.SplVM_in_class]
skip:67 [binder, in PreTalent22.SplVM_before_third_session]
skip:73 [binder, in PreTalent22.SplVM_in_class]
skip:73 [binder, in PreTalent22.SplVM_before_third_session]
skip:77 [binder, in PreTalent22.SplVM_in_class]
sk:34 [binder, in PreTalent22.SplVM]
sk:64 [binder, in PreTalent22.SplVM_in_class]
sk:64 [binder, in PreTalent22.SplVM_before_third_session]
Spl [library]
SplVM [library]
SplVM_in_class [library]
SplVM_before_third_session [library]
Spl_completed [library]
Spl_in_class [library]
stack [definition, in PreTalent22.SplVM]
stack [definition, in PreTalent22.SplVM_in_class]
stack [definition, in PreTalent22.SplVM_before_third_session]
stack_elem [inductive, in PreTalent22.SplVM]
stack_elem [inductive, in PreTalent22.SplVM_in_class]
stack_elem [inductive, in PreTalent22.SplVM_before_third_session]
Sub [constructor, in PreTalent22.Spl_in_class]
Sub [constructor, in PreTalent22.Spl_completed]
Sub [constructor, in PreTalent22.Spl]
Sub_typed [constructor, in PreTalent22.Spl_completed]
sub74 [definition, in PreTalent22.SplVM]
sub74 [definition, in PreTalent22.Spl_in_class]
sub74 [definition, in PreTalent22.SplVM_in_class]
sub74 [definition, in PreTalent22.Spl_completed]
sub74 [definition, in PreTalent22.SplVM_before_third_session]
sub74 [definition, in PreTalent22.Spl]
sum [definition, in PreTalent22.Arith]
sum [definition, in PreTalent22.Arith_in_class]
sum_S [lemma, in PreTalent22.Arith]
sum_S [lemma, in PreTalent22.Arith_in_class]
s'':31 [binder, in PreTalent22.SplVM_in_class]
s'':31 [binder, in PreTalent22.SplVM_before_third_session]
s'':35 [binder, in PreTalent22.SplVM_in_class]
s'':35 [binder, in PreTalent22.SplVM_before_third_session]
s'':41 [binder, in PreTalent22.SplVM_in_class]
s'':41 [binder, in PreTalent22.SplVM_before_third_session]
s'':45 [binder, in PreTalent22.SplVM_in_class]
s'':45 [binder, in PreTalent22.SplVM_before_third_session]
s'':49 [binder, in PreTalent22.SplVM_in_class]
s'':49 [binder, in PreTalent22.SplVM_before_third_session]
s'':53 [binder, in PreTalent22.SplVM_in_class]
s'':53 [binder, in PreTalent22.SplVM_before_third_session]
s'':57 [binder, in PreTalent22.SplVM_in_class]
s'':57 [binder, in PreTalent22.SplVM_before_third_session]
s':27 [binder, in PreTalent22.SplVM]
s':27 [binder, in PreTalent22.SplVM_in_class]
s':27 [binder, in PreTalent22.SplVM_before_third_session]
s':29 [binder, in PreTalent22.SplVM_in_class]
s':29 [binder, in PreTalent22.SplVM_before_third_session]
s':33 [binder, in PreTalent22.SplVM_in_class]
s':33 [binder, in PreTalent22.SplVM_before_third_session]
s':35 [binder, in PreTalent22.SplVM]
s':37 [binder, in PreTalent22.SplVM_in_class]
s':37 [binder, in PreTalent22.SplVM_before_third_session]
s':39 [binder, in PreTalent22.SplVM_in_class]
s':39 [binder, in PreTalent22.SplVM_before_third_session]
s':41 [binder, in PreTalent22.SplVM]
s':43 [binder, in PreTalent22.SplVM_in_class]
s':43 [binder, in PreTalent22.SplVM_before_third_session]
s':47 [binder, in PreTalent22.SplVM_in_class]
s':47 [binder, in PreTalent22.SplVM_before_third_session]
s':51 [binder, in PreTalent22.SplVM_in_class]
s':51 [binder, in PreTalent22.SplVM_before_third_session]
s':55 [binder, in PreTalent22.SplVM_in_class]
s':55 [binder, in PreTalent22.SplVM_before_third_session]
s':65 [binder, in PreTalent22.SplVM_in_class]
s':65 [binder, in PreTalent22.SplVM_before_third_session]
s':71 [binder, in PreTalent22.SplVM_in_class]
s':71 [binder, in PreTalent22.SplVM_before_third_session]
s:12 [binder, in PreTalent22.SplVM]
s:12 [binder, in PreTalent22.SplVM_in_class]
s:12 [binder, in PreTalent22.SplVM_before_third_session]
s:23 [binder, in PreTalent22.SplVM]
s:23 [binder, in PreTalent22.SplVM_in_class]
s:23 [binder, in PreTalent22.SplVM_before_third_session]
s:27 [binder, in PreTalent22.Compiler_in_class]
s:28 [binder, in PreTalent22.SplVM]
s:36 [binder, in PreTalent22.SplVM]
s:42 [binder, in PreTalent22.SplVM]
s:58 [binder, in PreTalent22.SplVM_in_class]
s:58 [binder, in PreTalent22.SplVM_before_third_session]
s:6 [binder, in PreTalent22.SplVM]
s:6 [binder, in PreTalent22.SplVM_in_class]
s:6 [binder, in PreTalent22.SplVM_before_third_session]
s:66 [binder, in PreTalent22.SplVM_in_class]
s:66 [binder, in PreTalent22.SplVM_before_third_session]
s:72 [binder, in PreTalent22.SplVM_in_class]
s:72 [binder, in PreTalent22.SplVM_before_third_session]
s:76 [binder, in PreTalent22.SplVM_in_class]
T
TBool [constructor, in PreTalent22.Spl_in_class]TBool [constructor, in PreTalent22.Spl_completed]
TBool [constructor, in PreTalent22.Spl]
TNum [constructor, in PreTalent22.Spl_in_class]
TNum [constructor, in PreTalent22.Spl_completed]
TNum [constructor, in PreTalent22.Spl]
tp:83 [binder, in PreTalent22.Spl_in_class]
tp:83 [binder, in PreTalent22.Spl_completed]
typ [inductive, in PreTalent22.Spl_in_class]
typ [inductive, in PreTalent22.Spl_completed]
typ [inductive, in PreTalent22.Spl]
typed [inductive, in PreTalent22.Spl_in_class]
typed [inductive, in PreTalent22.Spl_completed]
typed [inductive, in PreTalent22.Spl]
typed_soundness [lemma, in PreTalent22.Spl_in_class]
typed_soundness [lemma, in PreTalent22.Spl_completed]
typed_soundness [lemma, in PreTalent22.Spl]
typing_not_complete [lemma, in PreTalent22.Spl_in_class]
typing_not_complete [lemma, in PreTalent22.Spl_completed]
typing_not_complete [lemma, in PreTalent22.Spl]
t:100 [binder, in PreTalent22.Spl_completed]
t:102 [binder, in PreTalent22.Spl_completed]
t:104 [binder, in PreTalent22.Spl_completed]
t:6 [binder, in PreTalent22.Spl_in_class]
t:6 [binder, in PreTalent22.Spl_completed]
t:6 [binder, in PreTalent22.Spl]
t:64 [binder, in PreTalent22.Spl]
t:66 [binder, in PreTalent22.Spl]
t:68 [binder, in PreTalent22.Spl]
t:81 [binder, in PreTalent22.Spl_in_class]
t:81 [binder, in PreTalent22.Spl_completed]
t:85 [binder, in PreTalent22.Spl_in_class]
t:87 [binder, in PreTalent22.Spl_in_class]
t:89 [binder, in PreTalent22.Spl_in_class]
V
VMInstr [inductive, in PreTalent22.SplVM]VMInstr [inductive, in PreTalent22.SplVM_in_class]
VMInstr [inductive, in PreTalent22.SplVM_before_third_session]
VMProg [definition, in PreTalent22.SplVM]
VMProg [definition, in PreTalent22.SplVM_in_class]
VMProg [definition, in PreTalent22.SplVM_before_third_session]
vm_e2:21 [binder, in PreTalent22.Compiler]
vm_e1:20 [binder, in PreTalent22.Compiler]
vm_e2:19 [binder, in PreTalent22.Compiler]
vm_e1:18 [binder, in PreTalent22.Compiler]
vm_e2:17 [binder, in PreTalent22.Compiler]
vm_e1:16 [binder, in PreTalent22.Compiler]
vm_e2:15 [binder, in PreTalent22.Compiler]
vm_e1:14 [binder, in PreTalent22.Compiler]
vm_e2:13 [binder, in PreTalent22.Compiler]
vm_e1:12 [binder, in PreTalent22.Compiler]
vm_e:11 [binder, in PreTalent22.Compiler]
vm_e2:10 [binder, in PreTalent22.Compiler]
vm_e1:9 [binder, in PreTalent22.Compiler]
vm_e2:8 [binder, in PreTalent22.Compiler]
vm_e1:7 [binder, in PreTalent22.Compiler]
vm_f:6 [binder, in PreTalent22.Compiler]
vm_t:5 [binder, in PreTalent22.Compiler]
vm_c:4 [binder, in PreTalent22.Compiler]
vm_e2:21 [binder, in PreTalent22.Compiler_in_class]
vm_e1:20 [binder, in PreTalent22.Compiler_in_class]
vm_e2:19 [binder, in PreTalent22.Compiler_in_class]
vm_e1:18 [binder, in PreTalent22.Compiler_in_class]
vm_e2:17 [binder, in PreTalent22.Compiler_in_class]
vm_e1:16 [binder, in PreTalent22.Compiler_in_class]
vm_e2:15 [binder, in PreTalent22.Compiler_in_class]
vm_e1:14 [binder, in PreTalent22.Compiler_in_class]
vm_e2:13 [binder, in PreTalent22.Compiler_in_class]
vm_e1:12 [binder, in PreTalent22.Compiler_in_class]
vm_e:11 [binder, in PreTalent22.Compiler_in_class]
vm_e2:10 [binder, in PreTalent22.Compiler_in_class]
vm_e1:9 [binder, in PreTalent22.Compiler_in_class]
vm_e2:8 [binder, in PreTalent22.Compiler_in_class]
vm_e1:7 [binder, in PreTalent22.Compiler_in_class]
vm_f:6 [binder, in PreTalent22.Compiler_in_class]
vm_t:5 [binder, in PreTalent22.Compiler_in_class]
vm_c:4 [binder, in PreTalent22.Compiler_in_class]
W
when_bool_correct2 [lemma, in PreTalent22.Spl_in_class]when_bool_correct1 [lemma, in PreTalent22.Spl_in_class]
when_bool_not_Err [lemma, in PreTalent22.Spl_in_class]
when_bool [definition, in PreTalent22.Spl_in_class]
when_num_correct2 [lemma, in PreTalent22.Spl_in_class]
when_num_correct1 [lemma, in PreTalent22.Spl_in_class]
when_num_not_Err [lemma, in PreTalent22.Spl_in_class]
when_num [definition, in PreTalent22.Spl_in_class]
when_bool_correct2 [lemma, in PreTalent22.Spl_completed]
when_bool_correct1 [lemma, in PreTalent22.Spl_completed]
when_bool_not_Err [lemma, in PreTalent22.Spl_completed]
when_bool [definition, in PreTalent22.Spl_completed]
when_num_correct2 [lemma, in PreTalent22.Spl_completed]
when_num_correct1 [lemma, in PreTalent22.Spl_completed]
when_num_not_Err [lemma, in PreTalent22.Spl_completed]
when_num [definition, in PreTalent22.Spl_completed]
when_bool_correct2 [lemma, in PreTalent22.Spl]
when_bool_correct1 [lemma, in PreTalent22.Spl]
when_bool_not_Err [lemma, in PreTalent22.Spl]
when_bool [definition, in PreTalent22.Spl]
when_num_correct2 [lemma, in PreTalent22.Spl]
when_num_correct1 [lemma, in PreTalent22.Spl]
when_num_not_Err [lemma, in PreTalent22.Spl]
when_num [definition, in PreTalent22.Spl]
other
_ >>b= _ [notation, in PreTalent22.Spl_in_class]_ >>n= _ [notation, in PreTalent22.Spl_in_class]
_ >>b= _ [notation, in PreTalent22.Spl_completed]
_ >>n= _ [notation, in PreTalent22.Spl_completed]
_ >>b= _ [notation, in PreTalent22.Spl]
_ >>n= _ [notation, in PreTalent22.Spl]
Notation Index
other
_ >>b= _ [in PreTalent22.Spl_in_class]_ >>n= _ [in PreTalent22.Spl_in_class]
_ >>b= _ [in PreTalent22.Spl_completed]
_ >>n= _ [in PreTalent22.Spl_completed]
_ >>b= _ [in PreTalent22.Spl]
_ >>n= _ [in PreTalent22.Spl]
Binder Index
A
A:11 [in PreTalent22.SplVM]A:11 [in PreTalent22.SplVM_in_class]
A:11 [in PreTalent22.SplVM_before_third_session]
a:13 [in PreTalent22.SplVM]
a:13 [in PreTalent22.SplVM_in_class]
a:13 [in PreTalent22.SplVM_before_third_session]
A:5 [in PreTalent22.SplVM]
A:5 [in PreTalent22.SplVM_in_class]
A:5 [in PreTalent22.SplVM_before_third_session]
a:7 [in PreTalent22.SplVM]
a:7 [in PreTalent22.SplVM_in_class]
a:7 [in PreTalent22.SplVM_before_third_session]
B
b1:30 [in PreTalent22.SplVM_in_class]b1:30 [in PreTalent22.SplVM_before_third_session]
b1:34 [in PreTalent22.SplVM_in_class]
b1:34 [in PreTalent22.SplVM_before_third_session]
b1:55 [in PreTalent22.Spl_in_class]
b1:55 [in PreTalent22.Spl_completed]
b1:57 [in PreTalent22.Spl_in_class]
b1:57 [in PreTalent22.Spl_completed]
b2:28 [in PreTalent22.SplVM_in_class]
b2:28 [in PreTalent22.SplVM_before_third_session]
b2:32 [in PreTalent22.SplVM_in_class]
b2:32 [in PreTalent22.SplVM_before_third_session]
b2:56 [in PreTalent22.Spl_in_class]
b2:56 [in PreTalent22.Spl_completed]
b2:58 [in PreTalent22.Spl_in_class]
b2:58 [in PreTalent22.Spl_completed]
b:20 [in PreTalent22.SplVM]
b:20 [in PreTalent22.SplVM_in_class]
b:20 [in PreTalent22.SplVM_before_third_session]
b:25 [in PreTalent22.Compiler]
b:25 [in PreTalent22.Compiler_in_class]
b:26 [in PreTalent22.SplVM]
b:26 [in PreTalent22.Spl_in_class]
b:26 [in PreTalent22.SplVM_in_class]
b:26 [in PreTalent22.Spl_completed]
b:26 [in PreTalent22.SplVM_before_third_session]
b:26 [in PreTalent22.Spl]
b:36 [in PreTalent22.SplVM_in_class]
b:36 [in PreTalent22.SplVM_before_third_session]
b:37 [in PreTalent22.Spl_in_class]
b:37 [in PreTalent22.Spl_completed]
b:37 [in PreTalent22.Spl]
b:4 [in PreTalent22.SplVM]
b:4 [in PreTalent22.Spl_in_class]
b:4 [in PreTalent22.SplVM_in_class]
b:4 [in PreTalent22.Spl_completed]
b:4 [in PreTalent22.SplVM_before_third_session]
b:4 [in PreTalent22.Spl]
b:46 [in PreTalent22.Spl_in_class]
b:46 [in PreTalent22.Spl_completed]
b:46 [in PreTalent22.Spl]
b:50 [in PreTalent22.Spl_in_class]
b:50 [in PreTalent22.Spl_completed]
b:50 [in PreTalent22.Spl]
b:54 [in PreTalent22.Spl_in_class]
b:54 [in PreTalent22.Spl_completed]
b:54 [in PreTalent22.Spl]
b:59 [in PreTalent22.Spl_in_class]
b:59 [in PreTalent22.Spl_completed]
b:75 [in PreTalent22.Spl_in_class]
b:79 [in PreTalent22.Spl_in_class]
b:79 [in PreTalent22.Spl_completed]
C
c:5 [in PreTalent22.Spl_in_class]c:5 [in PreTalent22.Spl_completed]
c:5 [in PreTalent22.Spl]
c:80 [in PreTalent22.Spl_in_class]
c:80 [in PreTalent22.Spl_completed]
E
e1:10 [in PreTalent22.Spl_in_class]e1:10 [in PreTalent22.Spl_completed]
e1:10 [in PreTalent22.Spl]
e1:13 [in PreTalent22.Spl_in_class]
e1:13 [in PreTalent22.Spl_completed]
e1:13 [in PreTalent22.Spl]
e1:15 [in PreTalent22.Spl_in_class]
e1:15 [in PreTalent22.Spl_completed]
e1:15 [in PreTalent22.Spl]
e1:17 [in PreTalent22.Spl_in_class]
e1:17 [in PreTalent22.Spl_completed]
e1:17 [in PreTalent22.Spl]
e1:19 [in PreTalent22.Spl_in_class]
e1:19 [in PreTalent22.Spl_completed]
e1:19 [in PreTalent22.Spl]
e1:21 [in PreTalent22.Spl_in_class]
e1:21 [in PreTalent22.Spl_completed]
e1:21 [in PreTalent22.Spl]
e1:8 [in PreTalent22.Spl_in_class]
e1:8 [in PreTalent22.Spl_completed]
e1:8 [in PreTalent22.Spl]
e1:84 [in PreTalent22.Spl_completed]
e1:86 [in PreTalent22.Spl_completed]
e1:89 [in PreTalent22.Spl_completed]
e1:91 [in PreTalent22.Spl_completed]
e1:93 [in PreTalent22.Spl_completed]
e1:95 [in PreTalent22.Spl_completed]
e1:97 [in PreTalent22.Spl_completed]
e2:11 [in PreTalent22.Spl_in_class]
e2:11 [in PreTalent22.Spl_completed]
e2:11 [in PreTalent22.Spl]
e2:14 [in PreTalent22.Spl_in_class]
e2:14 [in PreTalent22.Spl_completed]
e2:14 [in PreTalent22.Spl]
e2:16 [in PreTalent22.Spl_in_class]
e2:16 [in PreTalent22.Spl_completed]
e2:16 [in PreTalent22.Spl]
e2:18 [in PreTalent22.Spl_in_class]
e2:18 [in PreTalent22.Spl_completed]
e2:18 [in PreTalent22.Spl]
e2:20 [in PreTalent22.Spl_in_class]
e2:20 [in PreTalent22.Spl_completed]
e2:20 [in PreTalent22.Spl]
e2:22 [in PreTalent22.Spl_in_class]
e2:22 [in PreTalent22.Spl_completed]
e2:22 [in PreTalent22.Spl]
e2:85 [in PreTalent22.Spl_completed]
e2:87 [in PreTalent22.Spl_completed]
e2:9 [in PreTalent22.Spl_in_class]
e2:9 [in PreTalent22.Spl_completed]
e2:9 [in PreTalent22.Spl]
e2:90 [in PreTalent22.Spl_completed]
e2:92 [in PreTalent22.Spl_completed]
e2:94 [in PreTalent22.Spl_completed]
e2:96 [in PreTalent22.Spl_completed]
e2:98 [in PreTalent22.Spl_completed]
e:1 [in PreTalent22.Compiler]
e:1 [in PreTalent22.Compiler_in_class]
e:101 [in PreTalent22.Spl_completed]
e:103 [in PreTalent22.Spl_completed]
e:12 [in PreTalent22.Spl_in_class]
e:12 [in PreTalent22.Spl_completed]
e:12 [in PreTalent22.Spl]
e:26 [in PreTalent22.Compiler]
e:26 [in PreTalent22.Compiler_in_class]
e:29 [in PreTalent22.Compiler_in_class]
e:51 [in PreTalent22.Spl_in_class]
e:51 [in PreTalent22.Spl_completed]
e:51 [in PreTalent22.Spl]
e:63 [in PreTalent22.Spl]
e:65 [in PreTalent22.Spl]
e:67 [in PreTalent22.Spl]
e:84 [in PreTalent22.Spl_in_class]
e:86 [in PreTalent22.Spl_in_class]
e:88 [in PreTalent22.Spl_in_class]
e:88 [in PreTalent22.Spl_completed]
e:99 [in PreTalent22.Spl_completed]
F
f:14 [in PreTalent22.SplVM]f:14 [in PreTalent22.SplVM_in_class]
f:14 [in PreTalent22.SplVM_before_third_session]
f:28 [in PreTalent22.Spl_in_class]
f:28 [in PreTalent22.Spl_completed]
f:28 [in PreTalent22.Spl]
f:31 [in PreTalent22.Spl_in_class]
f:31 [in PreTalent22.Spl_completed]
f:31 [in PreTalent22.Spl]
f:33 [in PreTalent22.Spl_in_class]
f:33 [in PreTalent22.Spl_completed]
f:33 [in PreTalent22.Spl]
f:36 [in PreTalent22.Spl_in_class]
f:36 [in PreTalent22.Spl_completed]
f:36 [in PreTalent22.Spl]
f:40 [in PreTalent22.Spl_in_class]
f:40 [in PreTalent22.Spl_completed]
f:40 [in PreTalent22.Spl]
f:43 [in PreTalent22.Spl_in_class]
f:43 [in PreTalent22.Spl_completed]
f:43 [in PreTalent22.Spl]
f:45 [in PreTalent22.Spl_in_class]
f:45 [in PreTalent22.Spl_completed]
f:45 [in PreTalent22.Spl]
f:48 [in PreTalent22.Spl_in_class]
f:48 [in PreTalent22.Spl_completed]
f:48 [in PreTalent22.Spl]
f:7 [in PreTalent22.Spl_in_class]
f:7 [in PreTalent22.Spl_completed]
f:7 [in PreTalent22.Spl]
f:8 [in PreTalent22.SplVM]
f:8 [in PreTalent22.SplVM_in_class]
f:8 [in PreTalent22.SplVM_before_third_session]
f:82 [in PreTalent22.Spl_in_class]
f:82 [in PreTalent22.Spl_completed]
I
i:24 [in PreTalent22.SplVM]i:24 [in PreTalent22.SplVM_in_class]
i:24 [in PreTalent22.SplVM_before_third_session]
J
j:21 [in PreTalent22.SplVM]j:21 [in PreTalent22.SplVM_in_class]
j:21 [in PreTalent22.SplVM_before_third_session]
j:22 [in PreTalent22.SplVM]
j:22 [in PreTalent22.SplVM_in_class]
j:22 [in PreTalent22.SplVM_before_third_session]
K
k:10 [in PreTalent22.Arith]k:13 [in PreTalent22.Arith]
k:17 [in PreTalent22.Arith_in_class]
k:20 [in PreTalent22.Arith_in_class]
L
l:14 [in PreTalent22.Arith]l:21 [in PreTalent22.Arith_in_class]
M
m:12 [in PreTalent22.Arith]m:12 [in PreTalent22.Arith_in_class]
m:14 [in PreTalent22.Arith_in_class]
m:16 [in PreTalent22.Arith_in_class]
m:19 [in PreTalent22.Arith_in_class]
m:4 [in PreTalent22.Arith_in_class]
m:7 [in PreTalent22.Arith]
m:9 [in PreTalent22.Arith]
N
n1:40 [in PreTalent22.SplVM_in_class]n1:40 [in PreTalent22.SplVM_before_third_session]
n1:44 [in PreTalent22.SplVM_in_class]
n1:44 [in PreTalent22.SplVM_before_third_session]
n1:48 [in PreTalent22.SplVM_in_class]
n1:48 [in PreTalent22.SplVM_before_third_session]
n1:52 [in PreTalent22.SplVM_in_class]
n1:52 [in PreTalent22.SplVM_before_third_session]
n1:56 [in PreTalent22.SplVM_in_class]
n1:56 [in PreTalent22.SplVM_before_third_session]
n1:60 [in PreTalent22.Spl_in_class]
n1:60 [in PreTalent22.Spl_completed]
n1:62 [in PreTalent22.Spl_in_class]
n1:62 [in PreTalent22.Spl_completed]
n1:64 [in PreTalent22.Spl_in_class]
n1:64 [in PreTalent22.Spl_completed]
n1:66 [in PreTalent22.Spl_in_class]
n1:66 [in PreTalent22.Spl_completed]
n1:68 [in PreTalent22.Spl_in_class]
n1:68 [in PreTalent22.Spl_completed]
n2:38 [in PreTalent22.SplVM_in_class]
n2:38 [in PreTalent22.SplVM_before_third_session]
n2:42 [in PreTalent22.SplVM_in_class]
n2:42 [in PreTalent22.SplVM_before_third_session]
n2:46 [in PreTalent22.SplVM_in_class]
n2:46 [in PreTalent22.SplVM_before_third_session]
n2:50 [in PreTalent22.SplVM_in_class]
n2:50 [in PreTalent22.SplVM_before_third_session]
n2:54 [in PreTalent22.SplVM_in_class]
n2:54 [in PreTalent22.SplVM_before_third_session]
n2:61 [in PreTalent22.Spl_in_class]
n2:61 [in PreTalent22.Spl_completed]
n2:63 [in PreTalent22.Spl_in_class]
n2:63 [in PreTalent22.Spl_completed]
n2:65 [in PreTalent22.Spl_in_class]
n2:65 [in PreTalent22.Spl_completed]
n2:67 [in PreTalent22.Spl_in_class]
n2:67 [in PreTalent22.Spl_completed]
n2:69 [in PreTalent22.Spl_in_class]
n2:69 [in PreTalent22.Spl_completed]
n:10 [in PreTalent22.Arith_in_class]
n:11 [in PreTalent22.Arith]
n:11 [in PreTalent22.Arith_in_class]
n:13 [in PreTalent22.Arith_in_class]
n:15 [in PreTalent22.Arith]
n:15 [in PreTalent22.Arith_in_class]
n:16 [in PreTalent22.Arith]
n:18 [in PreTalent22.Arith_in_class]
n:19 [in PreTalent22.SplVM]
n:19 [in PreTalent22.SplVM_in_class]
n:19 [in PreTalent22.SplVM_before_third_session]
n:22 [in PreTalent22.Arith_in_class]
n:23 [in PreTalent22.Arith_in_class]
n:24 [in PreTalent22.Compiler]
n:24 [in PreTalent22.Compiler_in_class]
n:25 [in PreTalent22.Spl_in_class]
n:25 [in PreTalent22.Spl_completed]
n:25 [in PreTalent22.Spl]
n:3 [in PreTalent22.SplVM]
n:3 [in PreTalent22.Spl_in_class]
n:3 [in PreTalent22.SplVM_in_class]
n:3 [in PreTalent22.Spl_completed]
n:3 [in PreTalent22.SplVM_before_third_session]
n:3 [in PreTalent22.Arith]
n:3 [in PreTalent22.Arith_in_class]
n:3 [in PreTalent22.Spl]
n:34 [in PreTalent22.Spl_in_class]
n:34 [in PreTalent22.Spl_completed]
n:34 [in PreTalent22.Spl]
n:38 [in PreTalent22.Spl_in_class]
n:38 [in PreTalent22.Spl_completed]
n:38 [in PreTalent22.Spl]
n:49 [in PreTalent22.Spl_in_class]
n:49 [in PreTalent22.Spl_completed]
n:49 [in PreTalent22.Spl]
n:59 [in PreTalent22.Spl]
n:6 [in PreTalent22.Arith]
n:62 [in PreTalent22.Spl]
n:7 [in PreTalent22.Arith_in_class]
n:74 [in PreTalent22.Spl_in_class]
n:74 [in PreTalent22.Spl_completed]
n:75 [in PreTalent22.Spl_completed]
n:78 [in PreTalent22.Spl_in_class]
n:78 [in PreTalent22.Spl_completed]
n:8 [in PreTalent22.Arith]
P
p1:38 [in PreTalent22.SplVM]p1:44 [in PreTalent22.SplVM]
p1:68 [in PreTalent22.SplVM_in_class]
p1:68 [in PreTalent22.SplVM_before_third_session]
p1:74 [in PreTalent22.SplVM_in_class]
p1:74 [in PreTalent22.SplVM_before_third_session]
p2:39 [in PreTalent22.SplVM]
p2:45 [in PreTalent22.SplVM]
p2:69 [in PreTalent22.SplVM_in_class]
p2:69 [in PreTalent22.SplVM_before_third_session]
p2:75 [in PreTalent22.SplVM_in_class]
p2:75 [in PreTalent22.SplVM_before_third_session]
p:30 [in PreTalent22.SplVM]
p:60 [in PreTalent22.SplVM_in_class]
p:60 [in PreTalent22.SplVM_before_third_session]
p:78 [in PreTalent22.SplVM_in_class]
R
r:27 [in PreTalent22.Spl_in_class]r:27 [in PreTalent22.Spl_completed]
r:27 [in PreTalent22.Spl]
r:30 [in PreTalent22.Spl_in_class]
r:30 [in PreTalent22.Spl_completed]
r:30 [in PreTalent22.Spl]
r:32 [in PreTalent22.Spl_in_class]
r:32 [in PreTalent22.Spl_completed]
r:32 [in PreTalent22.Spl]
r:35 [in PreTalent22.Spl_in_class]
r:35 [in PreTalent22.Spl_completed]
r:35 [in PreTalent22.Spl]
r:39 [in PreTalent22.Spl_in_class]
r:39 [in PreTalent22.Spl_completed]
r:39 [in PreTalent22.Spl]
r:42 [in PreTalent22.Spl_in_class]
r:42 [in PreTalent22.Spl_completed]
r:42 [in PreTalent22.Spl]
r:44 [in PreTalent22.Spl_in_class]
r:44 [in PreTalent22.Spl_completed]
r:44 [in PreTalent22.Spl]
r:47 [in PreTalent22.Spl_in_class]
r:47 [in PreTalent22.Spl_completed]
r:47 [in PreTalent22.Spl]
S
se:27 [in PreTalent22.Compiler]se:28 [in PreTalent22.Compiler_in_class]
se:30 [in PreTalent22.Compiler_in_class]
skip':40 [in PreTalent22.SplVM]
skip':70 [in PreTalent22.SplVM_in_class]
skip':70 [in PreTalent22.SplVM_before_third_session]
skip:29 [in PreTalent22.SplVM]
skip:37 [in PreTalent22.SplVM]
skip:43 [in PreTalent22.SplVM]
skip:59 [in PreTalent22.SplVM_in_class]
skip:59 [in PreTalent22.SplVM_before_third_session]
skip:67 [in PreTalent22.SplVM_in_class]
skip:67 [in PreTalent22.SplVM_before_third_session]
skip:73 [in PreTalent22.SplVM_in_class]
skip:73 [in PreTalent22.SplVM_before_third_session]
skip:77 [in PreTalent22.SplVM_in_class]
sk:34 [in PreTalent22.SplVM]
sk:64 [in PreTalent22.SplVM_in_class]
sk:64 [in PreTalent22.SplVM_before_third_session]
s'':31 [in PreTalent22.SplVM_in_class]
s'':31 [in PreTalent22.SplVM_before_third_session]
s'':35 [in PreTalent22.SplVM_in_class]
s'':35 [in PreTalent22.SplVM_before_third_session]
s'':41 [in PreTalent22.SplVM_in_class]
s'':41 [in PreTalent22.SplVM_before_third_session]
s'':45 [in PreTalent22.SplVM_in_class]
s'':45 [in PreTalent22.SplVM_before_third_session]
s'':49 [in PreTalent22.SplVM_in_class]
s'':49 [in PreTalent22.SplVM_before_third_session]
s'':53 [in PreTalent22.SplVM_in_class]
s'':53 [in PreTalent22.SplVM_before_third_session]
s'':57 [in PreTalent22.SplVM_in_class]
s'':57 [in PreTalent22.SplVM_before_third_session]
s':27 [in PreTalent22.SplVM]
s':27 [in PreTalent22.SplVM_in_class]
s':27 [in PreTalent22.SplVM_before_third_session]
s':29 [in PreTalent22.SplVM_in_class]
s':29 [in PreTalent22.SplVM_before_third_session]
s':33 [in PreTalent22.SplVM_in_class]
s':33 [in PreTalent22.SplVM_before_third_session]
s':35 [in PreTalent22.SplVM]
s':37 [in PreTalent22.SplVM_in_class]
s':37 [in PreTalent22.SplVM_before_third_session]
s':39 [in PreTalent22.SplVM_in_class]
s':39 [in PreTalent22.SplVM_before_third_session]
s':41 [in PreTalent22.SplVM]
s':43 [in PreTalent22.SplVM_in_class]
s':43 [in PreTalent22.SplVM_before_third_session]
s':47 [in PreTalent22.SplVM_in_class]
s':47 [in PreTalent22.SplVM_before_third_session]
s':51 [in PreTalent22.SplVM_in_class]
s':51 [in PreTalent22.SplVM_before_third_session]
s':55 [in PreTalent22.SplVM_in_class]
s':55 [in PreTalent22.SplVM_before_third_session]
s':65 [in PreTalent22.SplVM_in_class]
s':65 [in PreTalent22.SplVM_before_third_session]
s':71 [in PreTalent22.SplVM_in_class]
s':71 [in PreTalent22.SplVM_before_third_session]
s:12 [in PreTalent22.SplVM]
s:12 [in PreTalent22.SplVM_in_class]
s:12 [in PreTalent22.SplVM_before_third_session]
s:23 [in PreTalent22.SplVM]
s:23 [in PreTalent22.SplVM_in_class]
s:23 [in PreTalent22.SplVM_before_third_session]
s:27 [in PreTalent22.Compiler_in_class]
s:28 [in PreTalent22.SplVM]
s:36 [in PreTalent22.SplVM]
s:42 [in PreTalent22.SplVM]
s:58 [in PreTalent22.SplVM_in_class]
s:58 [in PreTalent22.SplVM_before_third_session]
s:6 [in PreTalent22.SplVM]
s:6 [in PreTalent22.SplVM_in_class]
s:6 [in PreTalent22.SplVM_before_third_session]
s:66 [in PreTalent22.SplVM_in_class]
s:66 [in PreTalent22.SplVM_before_third_session]
s:72 [in PreTalent22.SplVM_in_class]
s:72 [in PreTalent22.SplVM_before_third_session]
s:76 [in PreTalent22.SplVM_in_class]
T
tp:83 [in PreTalent22.Spl_in_class]tp:83 [in PreTalent22.Spl_completed]
t:100 [in PreTalent22.Spl_completed]
t:102 [in PreTalent22.Spl_completed]
t:104 [in PreTalent22.Spl_completed]
t:6 [in PreTalent22.Spl_in_class]
t:6 [in PreTalent22.Spl_completed]
t:6 [in PreTalent22.Spl]
t:64 [in PreTalent22.Spl]
t:66 [in PreTalent22.Spl]
t:68 [in PreTalent22.Spl]
t:81 [in PreTalent22.Spl_in_class]
t:81 [in PreTalent22.Spl_completed]
t:85 [in PreTalent22.Spl_in_class]
t:87 [in PreTalent22.Spl_in_class]
t:89 [in PreTalent22.Spl_in_class]
V
vm_e2:21 [in PreTalent22.Compiler]vm_e1:20 [in PreTalent22.Compiler]
vm_e2:19 [in PreTalent22.Compiler]
vm_e1:18 [in PreTalent22.Compiler]
vm_e2:17 [in PreTalent22.Compiler]
vm_e1:16 [in PreTalent22.Compiler]
vm_e2:15 [in PreTalent22.Compiler]
vm_e1:14 [in PreTalent22.Compiler]
vm_e2:13 [in PreTalent22.Compiler]
vm_e1:12 [in PreTalent22.Compiler]
vm_e:11 [in PreTalent22.Compiler]
vm_e2:10 [in PreTalent22.Compiler]
vm_e1:9 [in PreTalent22.Compiler]
vm_e2:8 [in PreTalent22.Compiler]
vm_e1:7 [in PreTalent22.Compiler]
vm_f:6 [in PreTalent22.Compiler]
vm_t:5 [in PreTalent22.Compiler]
vm_c:4 [in PreTalent22.Compiler]
vm_e2:21 [in PreTalent22.Compiler_in_class]
vm_e1:20 [in PreTalent22.Compiler_in_class]
vm_e2:19 [in PreTalent22.Compiler_in_class]
vm_e1:18 [in PreTalent22.Compiler_in_class]
vm_e2:17 [in PreTalent22.Compiler_in_class]
vm_e1:16 [in PreTalent22.Compiler_in_class]
vm_e2:15 [in PreTalent22.Compiler_in_class]
vm_e1:14 [in PreTalent22.Compiler_in_class]
vm_e2:13 [in PreTalent22.Compiler_in_class]
vm_e1:12 [in PreTalent22.Compiler_in_class]
vm_e:11 [in PreTalent22.Compiler_in_class]
vm_e2:10 [in PreTalent22.Compiler_in_class]
vm_e1:9 [in PreTalent22.Compiler_in_class]
vm_e2:8 [in PreTalent22.Compiler_in_class]
vm_e1:7 [in PreTalent22.Compiler_in_class]
vm_f:6 [in PreTalent22.Compiler_in_class]
vm_t:5 [in PreTalent22.Compiler_in_class]
vm_c:4 [in PreTalent22.Compiler_in_class]
Module Index
A
addition_multiplication [in PreTalent22.Arith]addition_multiplication [in PreTalent22.Arith_in_class]
N
Nat [in PreTalent22.Arith]Nat [in PreTalent22.Arith_in_class]
Library Index
A
ArithArith_in_class
C
CompilerCompiler_in_class
Coq
O
OvertureS
SplSplVM
SplVM_in_class
SplVM_before_third_session
Spl_completed
Spl_in_class
Lemma Index
A
add_assoc [in PreTalent22.Arith]add_comm [in PreTalent22.Arith]
add_assoc [in PreTalent22.Arith_in_class]
add_comm [in PreTalent22.Arith_in_class]
add_S [in PreTalent22.Arith_in_class]
add_zero [in PreTalent22.Arith_in_class]
C
compile_correct [in PreTalent22.Compiler]compile_correct [in PreTalent22.Compiler_in_class]
compile_correct_gen [in PreTalent22.Compiler_in_class]
E
eval_respects_types [in PreTalent22.Spl_in_class]eval_respects_types [in PreTalent22.Spl_completed]
eval_respects_types [in PreTalent22.Spl]
expand_add_mul [in PreTalent22.Arith]
expand_add_mul [in PreTalent22.Arith_in_class]
G
Gauss [in PreTalent22.Arith]Gauss [in PreTalent22.Arith_in_class]
R
runVMProg_jump [in PreTalent22.SplVM]runVMProg_app [in PreTalent22.SplVM]
runVMProg_whole_jump [in PreTalent22.SplVM_in_class]
runVMProg_jump [in PreTalent22.SplVM_in_class]
runVMProg_app [in PreTalent22.SplVM_in_class]
runVMProg_jump [in PreTalent22.SplVM_before_third_session]
runVMProg_app [in PreTalent22.SplVM_before_third_session]
S
sum_S [in PreTalent22.Arith]sum_S [in PreTalent22.Arith_in_class]
T
typed_soundness [in PreTalent22.Spl_in_class]typed_soundness [in PreTalent22.Spl_completed]
typed_soundness [in PreTalent22.Spl]
typing_not_complete [in PreTalent22.Spl_in_class]
typing_not_complete [in PreTalent22.Spl_completed]
typing_not_complete [in PreTalent22.Spl]
W
when_bool_correct2 [in PreTalent22.Spl_in_class]when_bool_correct1 [in PreTalent22.Spl_in_class]
when_bool_not_Err [in PreTalent22.Spl_in_class]
when_num_correct2 [in PreTalent22.Spl_in_class]
when_num_correct1 [in PreTalent22.Spl_in_class]
when_num_not_Err [in PreTalent22.Spl_in_class]
when_bool_correct2 [in PreTalent22.Spl_completed]
when_bool_correct1 [in PreTalent22.Spl_completed]
when_bool_not_Err [in PreTalent22.Spl_completed]
when_num_correct2 [in PreTalent22.Spl_completed]
when_num_correct1 [in PreTalent22.Spl_completed]
when_num_not_Err [in PreTalent22.Spl_completed]
when_bool_correct2 [in PreTalent22.Spl]
when_bool_correct1 [in PreTalent22.Spl]
when_bool_not_Err [in PreTalent22.Spl]
when_num_correct2 [in PreTalent22.Spl]
when_num_correct1 [in PreTalent22.Spl]
when_num_not_Err [in PreTalent22.Spl]
Constructor Index
A
Add [in PreTalent22.Spl_in_class]Add [in PreTalent22.Spl_completed]
Add [in PreTalent22.Spl]
Add_typed [in PreTalent22.Spl_completed]
And [in PreTalent22.Spl_in_class]
And [in PreTalent22.Spl_completed]
And [in PreTalent22.Spl]
And_typed [in PreTalent22.Spl_completed]
B
Bool [in PreTalent22.Spl_in_class]Bool [in PreTalent22.Spl_completed]
Bool [in PreTalent22.Spl]
BoolEl [in PreTalent22.SplVM]
BoolEl [in PreTalent22.SplVM_in_class]
BoolEl [in PreTalent22.SplVM_before_third_session]
BoolRes [in PreTalent22.Spl_in_class]
BoolRes [in PreTalent22.Spl_completed]
BoolRes [in PreTalent22.Spl]
BoolRes_typed [in PreTalent22.Spl_in_class]
BoolRes_typed [in PreTalent22.Spl_completed]
Bool_typed [in PreTalent22.Spl_in_class]
Bool_typed [in PreTalent22.Spl_completed]
bool_res_rel [in PreTalent22.Compiler]
bool_res_rel [in PreTalent22.Compiler_in_class]
C
CJump [in PreTalent22.SplVM]CJump [in PreTalent22.SplVM_in_class]
CJump [in PreTalent22.SplVM_before_third_session]
D
DoAdd [in PreTalent22.SplVM]DoAdd [in PreTalent22.SplVM_in_class]
DoAdd [in PreTalent22.SplVM_before_third_session]
DoAnd [in PreTalent22.SplVM]
DoAnd [in PreTalent22.SplVM_in_class]
DoAnd [in PreTalent22.SplVM_before_third_session]
DoEq [in PreTalent22.SplVM]
DoEq [in PreTalent22.SplVM_in_class]
DoEq [in PreTalent22.SplVM_before_third_session]
DoLe [in PreTalent22.SplVM]
DoLe [in PreTalent22.SplVM_in_class]
DoLe [in PreTalent22.SplVM_before_third_session]
DoMul [in PreTalent22.SplVM]
DoMul [in PreTalent22.SplVM_in_class]
DoMul [in PreTalent22.SplVM_before_third_session]
DoNot [in PreTalent22.SplVM]
DoNot [in PreTalent22.SplVM_in_class]
DoNot [in PreTalent22.SplVM_before_third_session]
DoOr [in PreTalent22.SplVM]
DoOr [in PreTalent22.SplVM_in_class]
DoOr [in PreTalent22.SplVM_before_third_session]
DoSub [in PreTalent22.SplVM]
DoSub [in PreTalent22.SplVM_in_class]
DoSub [in PreTalent22.SplVM_before_third_session]
E
Eq [in PreTalent22.Spl_in_class]Eq [in PreTalent22.Spl_completed]
Eq [in PreTalent22.Spl]
Eq_typed [in PreTalent22.Spl_completed]
Err [in PreTalent22.Spl_in_class]
Err [in PreTalent22.Spl_completed]
Err [in PreTalent22.Spl]
I
ITE [in PreTalent22.Spl_in_class]ITE [in PreTalent22.Spl_completed]
ITE [in PreTalent22.Spl]
ITE_typed [in PreTalent22.Spl_in_class]
ITE_typed [in PreTalent22.Spl_completed]
J
Jump [in PreTalent22.SplVM]Jump [in PreTalent22.SplVM_in_class]
Jump [in PreTalent22.SplVM_before_third_session]
L
Le [in PreTalent22.Spl_in_class]Le [in PreTalent22.Spl_completed]
Le [in PreTalent22.Spl]
Le_typed [in PreTalent22.Spl_completed]
M
Mul [in PreTalent22.Spl_in_class]Mul [in PreTalent22.Spl_completed]
Mul [in PreTalent22.Spl]
Mul_typed [in PreTalent22.Spl_completed]
N
Nat.O [in PreTalent22.Arith]Nat.O [in PreTalent22.Arith_in_class]
Nat.S [in PreTalent22.Arith]
Nat.S [in PreTalent22.Arith_in_class]
Not [in PreTalent22.Spl_in_class]
Not [in PreTalent22.Spl_completed]
Not [in PreTalent22.Spl]
Not_typed [in PreTalent22.Spl_completed]
Num [in PreTalent22.Spl_in_class]
Num [in PreTalent22.Spl_completed]
Num [in PreTalent22.Spl]
NumEl [in PreTalent22.SplVM]
NumEl [in PreTalent22.SplVM_in_class]
NumEl [in PreTalent22.SplVM_before_third_session]
NumRes [in PreTalent22.Spl_in_class]
NumRes [in PreTalent22.Spl_completed]
NumRes [in PreTalent22.Spl]
NumRes_typed [in PreTalent22.Spl_in_class]
NumRes_typed [in PreTalent22.Spl_completed]
NumRes_typed [in PreTalent22.Spl]
Num_typed [in PreTalent22.Spl_in_class]
Num_typed [in PreTalent22.Spl_completed]
num_res_rel [in PreTalent22.Compiler]
num_res_rel [in PreTalent22.Compiler_in_class]
Num_typed [in PreTalent22.Spl]
O
Or [in PreTalent22.Spl_in_class]Or [in PreTalent22.Spl_completed]
Or [in PreTalent22.Spl]
Or_typed [in PreTalent22.Spl_completed]
P
PushBool [in PreTalent22.SplVM]PushBool [in PreTalent22.SplVM_in_class]
PushBool [in PreTalent22.SplVM_before_third_session]
PushNum [in PreTalent22.SplVM]
PushNum [in PreTalent22.SplVM_in_class]
PushNum [in PreTalent22.SplVM_before_third_session]
S
Sub [in PreTalent22.Spl_in_class]Sub [in PreTalent22.Spl_completed]
Sub [in PreTalent22.Spl]
Sub_typed [in PreTalent22.Spl_completed]
T
TBool [in PreTalent22.Spl_in_class]TBool [in PreTalent22.Spl_completed]
TBool [in PreTalent22.Spl]
TNum [in PreTalent22.Spl_in_class]
TNum [in PreTalent22.Spl_completed]
TNum [in PreTalent22.Spl]
Inductive Index
E
expr [in PreTalent22.Spl_in_class]expr [in PreTalent22.Spl_completed]
expr [in PreTalent22.Spl]
N
Nat.nat [in PreTalent22.Arith]Nat.nat [in PreTalent22.Arith_in_class]
R
result [in PreTalent22.Spl_in_class]result [in PreTalent22.Spl_completed]
result [in PreTalent22.Spl]
result_rel [in PreTalent22.Compiler]
result_rel [in PreTalent22.Compiler_in_class]
res_typed [in PreTalent22.Spl_in_class]
res_typed [in PreTalent22.Spl_completed]
res_typed [in PreTalent22.Spl]
S
stack_elem [in PreTalent22.SplVM]stack_elem [in PreTalent22.SplVM_in_class]
stack_elem [in PreTalent22.SplVM_before_third_session]
T
typ [in PreTalent22.Spl_in_class]typ [in PreTalent22.Spl_completed]
typ [in PreTalent22.Spl]
typed [in PreTalent22.Spl_in_class]
typed [in PreTalent22.Spl_completed]
typed [in PreTalent22.Spl]
V
VMInstr [in PreTalent22.SplVM]VMInstr [in PreTalent22.SplVM_in_class]
VMInstr [in PreTalent22.SplVM_before_third_session]
Definition Index
A
addition_multiplication.add [in PreTalent22.Arith_in_class]add23 [in PreTalent22.SplVM]
add23 [in PreTalent22.Spl_in_class]
add23 [in PreTalent22.SplVM_in_class]
add23 [in PreTalent22.Spl_completed]
add23 [in PreTalent22.SplVM_before_third_session]
add23 [in PreTalent22.Spl]
B
bad_prog [in PreTalent22.SplVM]bad_prog [in PreTalent22.Spl_in_class]
bad_prog [in PreTalent22.SplVM_in_class]
bad_prog [in PreTalent22.Spl_completed]
bad_prog [in PreTalent22.SplVM_before_third_session]
bad_prog [in PreTalent22.Spl]
C
compile [in PreTalent22.Compiler]compile [in PreTalent22.Compiler_in_class]
E
eval [in PreTalent22.Spl_in_class]eval [in PreTalent22.Spl_completed]
eval [in PreTalent22.Spl]
I
if3le5 [in PreTalent22.SplVM]if3le5 [in PreTalent22.Spl_in_class]
if3le5 [in PreTalent22.SplVM_in_class]
if3le5 [in PreTalent22.Spl_completed]
if3le5 [in PreTalent22.SplVM_before_third_session]
if3le5 [in PreTalent22.Spl]
P
pop_bool [in PreTalent22.SplVM]pop_num [in PreTalent22.SplVM]
pop_bool [in PreTalent22.SplVM_in_class]
pop_num [in PreTalent22.SplVM_in_class]
pop_bool [in PreTalent22.SplVM_before_third_session]
pop_num [in PreTalent22.SplVM_before_third_session]
R
runVMInstr [in PreTalent22.SplVM]runVMInstr [in PreTalent22.SplVM_in_class]
runVMInstr [in PreTalent22.SplVM_before_third_session]
runVMProg [in PreTalent22.SplVM]
runVMProg [in PreTalent22.SplVM_in_class]
runVMProg [in PreTalent22.SplVM_before_third_session]
S
stack [in PreTalent22.SplVM]stack [in PreTalent22.SplVM_in_class]
stack [in PreTalent22.SplVM_before_third_session]
sub74 [in PreTalent22.SplVM]
sub74 [in PreTalent22.Spl_in_class]
sub74 [in PreTalent22.SplVM_in_class]
sub74 [in PreTalent22.Spl_completed]
sub74 [in PreTalent22.SplVM_before_third_session]
sub74 [in PreTalent22.Spl]
sum [in PreTalent22.Arith]
sum [in PreTalent22.Arith_in_class]
V
VMProg [in PreTalent22.SplVM]VMProg [in PreTalent22.SplVM_in_class]
VMProg [in PreTalent22.SplVM_before_third_session]
W
when_bool [in PreTalent22.Spl_in_class]when_num [in PreTalent22.Spl_in_class]
when_bool [in PreTalent22.Spl_completed]
when_num [in PreTalent22.Spl_completed]
when_bool [in PreTalent22.Spl]
when_num [in PreTalent22.Spl]
| 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 | (729 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 | (6 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 | (459 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 | (4 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 | (12 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 | (49 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 | (118 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 | (25 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 | (56 entries) |