| 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 | (126 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 | (2 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 | (2 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 | (17 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 | (41 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 | (9 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 | (49 entries) |
Global Index
A
Add [constructor, in PreTalent24.Spl]addition_multiplication [module, in PreTalent24.Arith]
add_assoc [lemma, in PreTalent24.Arith]
add_comm [lemma, in PreTalent24.Arith]
add23 [definition, in PreTalent24.Spl]
add23 [definition, in PreTalent24.SplVM]
And [constructor, in PreTalent24.Spl]
And_typed [constructor, in PreTalent24.Spl]
Arith [library]
B
bad_prog [definition, in PreTalent24.Spl]bad_prog [definition, in PreTalent24.SplVM]
Bool [constructor, in PreTalent24.Spl]
BoolEl [constructor, in PreTalent24.SplVM]
BoolRes [constructor, in PreTalent24.Spl]
BoolRes_typed [constructor, in PreTalent24.Spl]
bool_res_rel [constructor, in PreTalent24.Compiler]
Bool_typed [constructor, in PreTalent24.Spl]
C
CJump [constructor, in PreTalent24.SplVM]compile [definition, in PreTalent24.Compiler]
Compiler [library]
compile_correct [lemma, in PreTalent24.Compiler]
Coq [library]
D
DoAdd [constructor, in PreTalent24.SplVM]DoAnd [constructor, in PreTalent24.SplVM]
DoEq [constructor, in PreTalent24.SplVM]
DoLe [constructor, in PreTalent24.SplVM]
DoMul [constructor, in PreTalent24.SplVM]
DoNot [constructor, in PreTalent24.SplVM]
DoOr [constructor, in PreTalent24.SplVM]
DoSub [constructor, in PreTalent24.SplVM]
E
Eq [constructor, in PreTalent24.Spl]Err [constructor, in PreTalent24.Spl]
eval [definition, in PreTalent24.Spl]
eval_respects_types [lemma, in PreTalent24.Spl]
expand_add_mul [lemma, in PreTalent24.Arith]
expr [inductive, in PreTalent24.Spl]
expr_sind [definition, in PreTalent24.Spl]
expr_rec [definition, in PreTalent24.Spl]
expr_ind [definition, in PreTalent24.Spl]
expr_rect [definition, in PreTalent24.Spl]
G
Gauss [lemma, in PreTalent24.Arith]I
IFE_typed [constructor, in PreTalent24.Spl]if3le5 [definition, in PreTalent24.Spl]
if3le5 [definition, in PreTalent24.SplVM]
ITE [constructor, in PreTalent24.Spl]
J
Jump [constructor, in PreTalent24.SplVM]L
Le [constructor, in PreTalent24.Spl]Le_typed [constructor, in PreTalent24.Spl]
M
Mul [constructor, in PreTalent24.Spl]N
Nat [module, in PreTalent24.Arith]Nat.nat [inductive, in PreTalent24.Arith]
Nat.nat_sind [definition, in PreTalent24.Arith]
Nat.nat_rec [definition, in PreTalent24.Arith]
Nat.nat_ind [definition, in PreTalent24.Arith]
Nat.nat_rect [definition, in PreTalent24.Arith]
Nat.O [constructor, in PreTalent24.Arith]
Nat.S [constructor, in PreTalent24.Arith]
Not [constructor, in PreTalent24.Spl]
Num [constructor, in PreTalent24.Spl]
NumEl [constructor, in PreTalent24.SplVM]
NumRes [constructor, in PreTalent24.Spl]
NumRes_typed [constructor, in PreTalent24.Spl]
num_res_rel [constructor, in PreTalent24.Compiler]
Num_typed [constructor, in PreTalent24.Spl]
O
Or [constructor, in PreTalent24.Spl]Overture [library]
P
pop_bool [definition, in PreTalent24.SplVM]pop_num [definition, in PreTalent24.SplVM]
PushBool [constructor, in PreTalent24.SplVM]
PushNum [constructor, in PreTalent24.SplVM]
R
result [inductive, in PreTalent24.Spl]result_rel_sind [definition, in PreTalent24.Compiler]
result_rel_ind [definition, in PreTalent24.Compiler]
result_rel [inductive, in PreTalent24.Compiler]
result_sind [definition, in PreTalent24.Spl]
result_rec [definition, in PreTalent24.Spl]
result_ind [definition, in PreTalent24.Spl]
result_rect [definition, in PreTalent24.Spl]
res_typed_sind [definition, in PreTalent24.Spl]
res_typed_ind [definition, in PreTalent24.Spl]
res_typed [inductive, in PreTalent24.Spl]
runVMInstr [definition, in PreTalent24.SplVM]
runVMProg [definition, in PreTalent24.SplVM]
runVMProg_jump [lemma, in PreTalent24.SplVM]
runVMProg_app [lemma, in PreTalent24.SplVM]
S
Spl [library]SplVM [library]
stack [definition, in PreTalent24.SplVM]
stack_elem_sind [definition, in PreTalent24.SplVM]
stack_elem_rec [definition, in PreTalent24.SplVM]
stack_elem_ind [definition, in PreTalent24.SplVM]
stack_elem_rect [definition, in PreTalent24.SplVM]
stack_elem [inductive, in PreTalent24.SplVM]
Sub [constructor, in PreTalent24.Spl]
sub74 [definition, in PreTalent24.Spl]
sub74 [definition, in PreTalent24.SplVM]
sum [definition, in PreTalent24.Arith]
sum_S [lemma, in PreTalent24.Arith]
T
TBool [constructor, in PreTalent24.Spl]TNum [constructor, in PreTalent24.Spl]
typ [inductive, in PreTalent24.Spl]
typed [inductive, in PreTalent24.Spl]
typed_soundness [lemma, in PreTalent24.Spl]
typed_sind [definition, in PreTalent24.Spl]
typed_ind [definition, in PreTalent24.Spl]
typing_not_complete [lemma, in PreTalent24.Spl]
typ_sind [definition, in PreTalent24.Spl]
typ_rec [definition, in PreTalent24.Spl]
typ_ind [definition, in PreTalent24.Spl]
typ_rect [definition, in PreTalent24.Spl]
V
VMInstr [inductive, in PreTalent24.SplVM]VMInstr_sind [definition, in PreTalent24.SplVM]
VMInstr_rec [definition, in PreTalent24.SplVM]
VMInstr_ind [definition, in PreTalent24.SplVM]
VMInstr_rect [definition, in PreTalent24.SplVM]
VMProg [definition, in PreTalent24.SplVM]
W
when_bool_correct2 [lemma, in PreTalent24.Spl]when_bool_correct1 [lemma, in PreTalent24.Spl]
when_bool_not_Err [lemma, in PreTalent24.Spl]
when_bool [definition, in PreTalent24.Spl]
when_num_correct2 [lemma, in PreTalent24.Spl]
when_num_correct1 [lemma, in PreTalent24.Spl]
when_num_not_Err [lemma, in PreTalent24.Spl]
when_num [definition, in PreTalent24.Spl]
other
_ >>b= _ [notation, in PreTalent24.Spl]_ >>n= _ [notation, in PreTalent24.Spl]
Notation Index
other
_ >>b= _ [in PreTalent24.Spl]_ >>n= _ [in PreTalent24.Spl]
Module Index
A
addition_multiplication [in PreTalent24.Arith]N
Nat [in PreTalent24.Arith]Library Index
A
ArithC
CompilerCoq
O
OvertureS
SplSplVM
Lemma Index
A
add_assoc [in PreTalent24.Arith]add_comm [in PreTalent24.Arith]
C
compile_correct [in PreTalent24.Compiler]E
eval_respects_types [in PreTalent24.Spl]expand_add_mul [in PreTalent24.Arith]
G
Gauss [in PreTalent24.Arith]R
runVMProg_jump [in PreTalent24.SplVM]runVMProg_app [in PreTalent24.SplVM]
S
sum_S [in PreTalent24.Arith]T
typed_soundness [in PreTalent24.Spl]typing_not_complete [in PreTalent24.Spl]
W
when_bool_correct2 [in PreTalent24.Spl]when_bool_correct1 [in PreTalent24.Spl]
when_bool_not_Err [in PreTalent24.Spl]
when_num_correct2 [in PreTalent24.Spl]
when_num_correct1 [in PreTalent24.Spl]
when_num_not_Err [in PreTalent24.Spl]
Constructor Index
A
Add [in PreTalent24.Spl]And [in PreTalent24.Spl]
And_typed [in PreTalent24.Spl]
B
Bool [in PreTalent24.Spl]BoolEl [in PreTalent24.SplVM]
BoolRes [in PreTalent24.Spl]
BoolRes_typed [in PreTalent24.Spl]
bool_res_rel [in PreTalent24.Compiler]
Bool_typed [in PreTalent24.Spl]
C
CJump [in PreTalent24.SplVM]D
DoAdd [in PreTalent24.SplVM]DoAnd [in PreTalent24.SplVM]
DoEq [in PreTalent24.SplVM]
DoLe [in PreTalent24.SplVM]
DoMul [in PreTalent24.SplVM]
DoNot [in PreTalent24.SplVM]
DoOr [in PreTalent24.SplVM]
DoSub [in PreTalent24.SplVM]
E
Eq [in PreTalent24.Spl]Err [in PreTalent24.Spl]
I
IFE_typed [in PreTalent24.Spl]ITE [in PreTalent24.Spl]
J
Jump [in PreTalent24.SplVM]L
Le [in PreTalent24.Spl]Le_typed [in PreTalent24.Spl]
M
Mul [in PreTalent24.Spl]N
Nat.O [in PreTalent24.Arith]Nat.S [in PreTalent24.Arith]
Not [in PreTalent24.Spl]
Num [in PreTalent24.Spl]
NumEl [in PreTalent24.SplVM]
NumRes [in PreTalent24.Spl]
NumRes_typed [in PreTalent24.Spl]
num_res_rel [in PreTalent24.Compiler]
Num_typed [in PreTalent24.Spl]
O
Or [in PreTalent24.Spl]P
PushBool [in PreTalent24.SplVM]PushNum [in PreTalent24.SplVM]
S
Sub [in PreTalent24.Spl]T
TBool [in PreTalent24.Spl]TNum [in PreTalent24.Spl]
Inductive Index
E
expr [in PreTalent24.Spl]N
Nat.nat [in PreTalent24.Arith]R
result [in PreTalent24.Spl]result_rel [in PreTalent24.Compiler]
res_typed [in PreTalent24.Spl]
S
stack_elem [in PreTalent24.SplVM]T
typ [in PreTalent24.Spl]typed [in PreTalent24.Spl]
V
VMInstr [in PreTalent24.SplVM]Definition Index
A
add23 [in PreTalent24.Spl]add23 [in PreTalent24.SplVM]
B
bad_prog [in PreTalent24.Spl]bad_prog [in PreTalent24.SplVM]
C
compile [in PreTalent24.Compiler]E
eval [in PreTalent24.Spl]expr_sind [in PreTalent24.Spl]
expr_rec [in PreTalent24.Spl]
expr_ind [in PreTalent24.Spl]
expr_rect [in PreTalent24.Spl]
I
if3le5 [in PreTalent24.Spl]if3le5 [in PreTalent24.SplVM]
N
Nat.nat_sind [in PreTalent24.Arith]Nat.nat_rec [in PreTalent24.Arith]
Nat.nat_ind [in PreTalent24.Arith]
Nat.nat_rect [in PreTalent24.Arith]
P
pop_bool [in PreTalent24.SplVM]pop_num [in PreTalent24.SplVM]
R
result_rel_sind [in PreTalent24.Compiler]result_rel_ind [in PreTalent24.Compiler]
result_sind [in PreTalent24.Spl]
result_rec [in PreTalent24.Spl]
result_ind [in PreTalent24.Spl]
result_rect [in PreTalent24.Spl]
res_typed_sind [in PreTalent24.Spl]
res_typed_ind [in PreTalent24.Spl]
runVMInstr [in PreTalent24.SplVM]
runVMProg [in PreTalent24.SplVM]
S
stack [in PreTalent24.SplVM]stack_elem_sind [in PreTalent24.SplVM]
stack_elem_rec [in PreTalent24.SplVM]
stack_elem_ind [in PreTalent24.SplVM]
stack_elem_rect [in PreTalent24.SplVM]
sub74 [in PreTalent24.Spl]
sub74 [in PreTalent24.SplVM]
sum [in PreTalent24.Arith]
T
typed_sind [in PreTalent24.Spl]typed_ind [in PreTalent24.Spl]
typ_sind [in PreTalent24.Spl]
typ_rec [in PreTalent24.Spl]
typ_ind [in PreTalent24.Spl]
typ_rect [in PreTalent24.Spl]
V
VMInstr_sind [in PreTalent24.SplVM]VMInstr_rec [in PreTalent24.SplVM]
VMInstr_ind [in PreTalent24.SplVM]
VMInstr_rect [in PreTalent24.SplVM]
VMProg [in PreTalent24.SplVM]
W
when_bool [in PreTalent24.Spl]when_num [in PreTalent24.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 | (126 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 | (2 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 | (2 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 | (17 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 | (41 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 | (9 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 | (49 entries) |