| 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 | (292 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 | (1 entry) |
| 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 | (175 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 | (35 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 | (13 entries) |
| Abbreviation Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (5 entries) |
| 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 | (55 entries) |
Global Index
A
abs [constructor, in Stlc.Definitions]aeq [inductive, in Stlc.Nominal]
aeq_nom_to_exp [lemma, in Stlc.Connect]
aeq_app [constructor, in Stlc.Nominal]
aeq_abs_diff [constructor, in Stlc.Nominal]
aeq_abs_same [constructor, in Stlc.Nominal]
aeq_var [constructor, in Stlc.Nominal]
aeq1 [definition, in Stlc.Nominal]
app [constructor, in Stlc.Definitions]
append_assoc_demo [lemma, in Stlc.Lec2]
apply_stack_fresh_eq [lemma, in Stlc.Connect]
apply_heap_get [lemma, in Stlc.Connect]
apply_stack_cong [lemma, in Stlc.Connect]
apply_heap_open [lemma, in Stlc.Connect]
apply_heap_app [lemma, in Stlc.Connect]
apply_heap_abs [lemma, in Stlc.Connect]
apply_heap_lc [lemma, in Stlc.Connect]
apply_stack [definition, in Stlc.Connect]
apply_heap [definition, in Stlc.Connect]
B
binds_demo [lemma, in Stlc.Lec2]body_exp_wrt_exp [definition, in Stlc.Lemmas]
C
close_exp_wrt_exp_freshen [lemma, in Stlc.Connect]close_exp_wrt_exp_lc_exp [lemma, in Stlc.Lemmas]
close_exp_wrt_exp_rec_degree_exp_wrt_exp [lemma, in Stlc.Lemmas]
close_exp_wrt_exp_rec_degree_exp_wrt_exp_mutual [lemma, in Stlc.Lemmas]
close_exp_wrt_exp_open_exp_wrt_exp [lemma, in Stlc.Lemmas]
close_exp_wrt_exp_rec_open_exp_wrt_exp_rec [lemma, in Stlc.Lemmas]
close_exp_wrt_exp_rec_open_exp_wrt_exp_rec_mutual [lemma, in Stlc.Lemmas]
close_exp_wrt_exp_inj [lemma, in Stlc.Lemmas]
close_exp_wrt_exp_rec_inj [lemma, in Stlc.Lemmas]
close_exp_wrt_exp_rec_inj_mutual [lemma, in Stlc.Lemmas]
close_exp_wrt_exp [definition, in Stlc.Lemmas]
close_exp_wrt_exp_rec [definition, in Stlc.Lemmas]
cofinite_exists [lemma, in Stlc.Lec2]
combine [lemma, in Stlc.Connect]
configuration [definition, in Stlc.Nominal]
conf1 [definition, in Stlc.Connect]
Connect [library]
ctx [definition, in Stlc.Definitions]
D
decode [definition, in Stlc.Connect]decode_lc [lemma, in Stlc.Connect]
decode1 [definition, in Stlc.Connect]
Definitions [library]
degree_exp_wrt_exp_of_lc_exp [lemma, in Stlc.Lemmas]
degree_exp_wrt_exp_of_lc_exp_mutual [lemma, in Stlc.Lemmas]
degree_exp_wrt_exp_open_exp_wrt_exp_inv [lemma, in Stlc.Lemmas]
degree_exp_wrt_exp_open_exp_wrt_exp_rec_inv [lemma, in Stlc.Lemmas]
degree_exp_wrt_exp_open_exp_wrt_exp_rec_inv_mutual [lemma, in Stlc.Lemmas]
degree_exp_wrt_exp_open_exp_wrt_exp [lemma, in Stlc.Lemmas]
degree_exp_wrt_exp_open_exp_wrt_exp_rec [lemma, in Stlc.Lemmas]
degree_exp_wrt_exp_open_exp_wrt_exp_rec_mutual [lemma, in Stlc.Lemmas]
degree_exp_wrt_exp_close_exp_wrt_exp_inv [lemma, in Stlc.Lemmas]
degree_exp_wrt_exp_close_exp_wrt_exp_rec_inv [lemma, in Stlc.Lemmas]
degree_exp_wrt_exp_close_exp_wrt_exp_rec_inv_mutual [lemma, in Stlc.Lemmas]
degree_exp_wrt_exp_close_exp_wrt_exp [lemma, in Stlc.Lemmas]
degree_exp_wrt_exp_close_exp_wrt_exp_rec [lemma, in Stlc.Lemmas]
degree_exp_wrt_exp_close_exp_wrt_exp_rec_mutual [lemma, in Stlc.Lemmas]
degree_exp_wrt_exp_O [lemma, in Stlc.Lemmas]
degree_exp_wrt_exp_S [lemma, in Stlc.Lemmas]
degree_exp_wrt_exp_S_mutual [lemma, in Stlc.Lemmas]
degree_exp_wrt_exp_mutind [definition, in Stlc.Lemmas]
degree_exp_wrt_exp_ind' [definition, in Stlc.Lemmas]
degree_wrt_exp_app [constructor, in Stlc.Lemmas]
degree_wrt_exp_var_b [constructor, in Stlc.Lemmas]
degree_wrt_exp_var_f [constructor, in Stlc.Lemmas]
degree_wrt_exp_abs [constructor, in Stlc.Lemmas]
degree_exp_wrt_exp [inductive, in Stlc.Lemmas]
demo_lc [lemma, in Stlc.Lec1]
demo_open [lemma, in Stlc.Lec1]
demo_subst1 [definition, in Stlc.Lec1]
demo_rep3 [definition, in Stlc.Lec1]
demo_rep2 [definition, in Stlc.Lec1]
demo_rep1 [definition, in Stlc.Lec1]
demo_rep2 [definition, in Stlc.Nominal]
demo_rep1 [definition, in Stlc.Nominal]
dom_demo [lemma, in Stlc.Lec2]
Done [constructor, in Stlc.Nominal]
E
Error [constructor, in Stlc.Nominal]exists_cofinite [lemma, in Stlc.Lec2]
exp [inductive, in Stlc.Definitions]
exp_mutrec [definition, in Stlc.Lemmas]
exp_rec' [definition, in Stlc.Lemmas]
exp_mutind [definition, in Stlc.Lemmas]
exp_ind' [definition, in Stlc.Lemmas]
F
frame [inductive, in Stlc.Nominal]fsetdec_demo [lemma, in Stlc.Lec1]
fv_exp_open_exp_wrt_exp_upper [lemma, in Stlc.Lec1]
fv_exp_subst_exp_upper [lemma, in Stlc.Lec1]
fv_exp_subst_exp_fresh [lemma, in Stlc.Lec1]
fv_exp_subst_exp_notin [lemma, in Stlc.Lec1]
fv_stack [definition, in Stlc.Connect]
fv_nom_fv_exp_eq [lemma, in Stlc.Connect]
fv_in_dom [lemma, in Stlc.Lec2]
fv_nom_swap [lemma, in Stlc.Nominal]
fv_nom_rep1 [definition, in Stlc.Nominal]
fv_nom [definition, in Stlc.Nominal]
fv_exp [definition, in Stlc.Definitions]
fv_exp_subst_exp_upper [lemma, in Stlc.Lemmas]
fv_exp_subst_exp_upper_mutual [lemma, in Stlc.Lemmas]
fv_exp_subst_exp_notin [lemma, in Stlc.Lemmas]
fv_exp_subst_exp_notin_mutual [lemma, in Stlc.Lemmas]
fv_exp_subst_exp_lower [lemma, in Stlc.Lemmas]
fv_exp_subst_exp_lower_mutual [lemma, in Stlc.Lemmas]
fv_exp_subst_exp_fresh [lemma, in Stlc.Lemmas]
fv_exp_subst_exp_fresh_mutual [lemma, in Stlc.Lemmas]
fv_exp_open_exp_wrt_exp_upper [lemma, in Stlc.Lemmas]
fv_exp_open_exp_wrt_exp_rec_upper [lemma, in Stlc.Lemmas]
fv_exp_open_exp_wrt_exp_rec_upper_mutual [lemma, in Stlc.Lemmas]
fv_exp_open_exp_wrt_exp_lower [lemma, in Stlc.Lemmas]
fv_exp_open_exp_wrt_exp_rec_lower [lemma, in Stlc.Lemmas]
fv_exp_open_exp_wrt_exp_rec_lower_mutual [lemma, in Stlc.Lemmas]
fv_exp_close_exp_wrt_exp [lemma, in Stlc.Lemmas]
fv_exp_close_exp_wrt_exp_rec [lemma, in Stlc.Lemmas]
fv_exp_close_exp_wrt_exp_rec_mutual [lemma, in Stlc.Lemmas]
H
heap [definition, in Stlc.Nominal]I
initconf [definition, in Stlc.Nominal]in_fv_nom_equivariance [lemma, in Stlc.Nominal]
isVal [definition, in Stlc.Nominal]
is_value [definition, in Stlc.Definitions]
L
lc_abs_exists [lemma, in Stlc.Lec1]lc_app [constructor, in Stlc.Definitions]
lc_abs [constructor, in Stlc.Definitions]
lc_var_f [constructor, in Stlc.Definitions]
lc_exp [inductive, in Stlc.Definitions]
lc_body_abs_1 [lemma, in Stlc.Lemmas]
lc_body_exp_wrt_exp [lemma, in Stlc.Lemmas]
lc_abs_exists [lemma, in Stlc.Lemmas]
lc_exp_of_degree [lemma, in Stlc.Lemmas]
lc_exp_of_degree_size_mutual [lemma, in Stlc.Lemmas]
lc_exp_mutind [definition, in Stlc.Lemmas]
lc_exp_ind' [definition, in Stlc.Lemmas]
Lec1 [library]
Lec2 [library]
Lemmas [library]
M
machine_is_scoped [lemma, in Stlc.Connect]machine_step [definition, in Stlc.Nominal]
N
Nominal [library]nom_to_exp_eq_aeq [lemma, in Stlc.Connect]
nom_to_exp_lc [lemma, in Stlc.Connect]
nom_to_exp [definition, in Stlc.Connect]
notin_fv_nom_equivariance [lemma, in Stlc.Nominal]
n_app2 [constructor, in Stlc.Nominal]
n_app [constructor, in Stlc.Nominal]
n_abs [constructor, in Stlc.Nominal]
n_var [constructor, in Stlc.Nominal]
n_exp [inductive, in Stlc.Nominal]
O
open_exp_wrt_exp [definition, in Stlc.Definitions]open_exp_wrt_exp_rec [definition, in Stlc.Definitions]
open_exp_wrt_exp_lc_exp [lemma, in Stlc.Lemmas]
open_exp_wrt_exp_rec_degree_exp_wrt_exp [lemma, in Stlc.Lemmas]
open_exp_wrt_exp_rec_degree_exp_wrt_exp_mutual [lemma, in Stlc.Lemmas]
open_exp_wrt_exp_inj [lemma, in Stlc.Lemmas]
open_exp_wrt_exp_rec_inj [lemma, in Stlc.Lemmas]
open_exp_wrt_exp_rec_inj_mutual [lemma, in Stlc.Lemmas]
open_exp_wrt_exp_close_exp_wrt_exp [lemma, in Stlc.Lemmas]
open_exp_wrt_exp_rec_close_exp_wrt_exp_rec [lemma, in Stlc.Lemmas]
open_exp_wrt_exp_rec_close_exp_wrt_exp_rec_mutual [lemma, in Stlc.Lemmas]
P
preservation [lemma, in Stlc.Lec2]progress [lemma, in Stlc.Lec2]
S
scoped_conf_witness [constructor, in Stlc.Connect]scoped_conf [inductive, in Stlc.Connect]
scoped_cons [constructor, in Stlc.Connect]
scoped_nil [constructor, in Stlc.Connect]
scoped_heap [inductive, in Stlc.Connect]
shuffle_swap [lemma, in Stlc.Nominal]
simpl_env_demo [lemma, in Stlc.Lec2]
simulate_error [lemma, in Stlc.Connect]
simulate_done [lemma, in Stlc.Connect]
simulate_step [lemma, in Stlc.Connect]
size [definition, in Stlc.Nominal]
size_exp_open_exp_wrt_exp_var [lemma, in Stlc.Lemmas]
size_exp_open_exp_wrt_exp_rec_var [lemma, in Stlc.Lemmas]
size_exp_open_exp_wrt_exp_rec_var_mutual [lemma, in Stlc.Lemmas]
size_exp_open_exp_wrt_exp [lemma, in Stlc.Lemmas]
size_exp_open_exp_wrt_exp_rec [lemma, in Stlc.Lemmas]
size_exp_open_exp_wrt_exp_rec_mutual [lemma, in Stlc.Lemmas]
size_exp_close_exp_wrt_exp [lemma, in Stlc.Lemmas]
size_exp_close_exp_wrt_exp_rec [lemma, in Stlc.Lemmas]
size_exp_close_exp_wrt_exp_rec_mutual [lemma, in Stlc.Lemmas]
size_exp_min [lemma, in Stlc.Lemmas]
size_exp_min_mutual [lemma, in Stlc.Lemmas]
size_typ_min [lemma, in Stlc.Lemmas]
size_typ_min_mutual [lemma, in Stlc.Lemmas]
size_exp [definition, in Stlc.Lemmas]
size_typ [definition, in Stlc.Lemmas]
stack [abbreviation, in Stlc.Nominal]
Step [inductive, in Stlc.Nominal]
step [inductive, in Stlc.Definitions]
step_lc_exp2 [lemma, in Stlc.Lec1]
step_lc_exp1 [lemma, in Stlc.Lec1]
step_app [constructor, in Stlc.Definitions]
step_beta [constructor, in Stlc.Definitions]
StlcNotations [module, in Stlc.Definitions]
StlcNotations.open [abbreviation, in Stlc.Definitions]
_ ^ _ (exp_scope) [notation, in Stlc.Definitions]
[ _ ~> _ ] _ (exp_scope) [notation, in Stlc.Definitions]
subst [definition, in Stlc.Nominal]
subst_exp_lc_exp [lemma, in Stlc.Lec1]
subst_lc0 [lemma, in Stlc.Lec1]
subst_exp_intro [lemma, in Stlc.Lec1]
subst_var [lemma, in Stlc.Lec1]
subst_exp_open_exp_wrt_exp [lemma, in Stlc.Lec1]
subst_exp_fresh_same [lemma, in Stlc.Lec1]
subst_exp_fresh_eq [lemma, in Stlc.Lec1]
subst_same [lemma, in Stlc.Lec1]
subst_neq_var [lemma, in Stlc.Lec1]
subst_eq_var [lemma, in Stlc.Lec1]
subst_abs [lemma, in Stlc.Nominal]
subst_app [lemma, in Stlc.Nominal]
subst_neq_var [lemma, in Stlc.Nominal]
subst_eq_var [lemma, in Stlc.Nominal]
subst_size [lemma, in Stlc.Nominal]
subst_rec [definition, in Stlc.Nominal]
subst_exp [definition, in Stlc.Definitions]
subst_exp_intro [lemma, in Stlc.Lemmas]
subst_exp_intro_rec [lemma, in Stlc.Lemmas]
subst_exp_abs [lemma, in Stlc.Lemmas]
subst_exp_close_exp_wrt_exp_open_exp_wrt_exp [lemma, in Stlc.Lemmas]
subst_exp_close_exp_wrt_exp_rec_open_exp_wrt_exp_rec [lemma, in Stlc.Lemmas]
subst_exp_close_exp_wrt_exp_rec_open_exp_wrt_exp_rec_mutual [lemma, in Stlc.Lemmas]
subst_exp_subst_exp [lemma, in Stlc.Lemmas]
subst_exp_subst_exp_mutual [lemma, in Stlc.Lemmas]
subst_exp_spec [lemma, in Stlc.Lemmas]
subst_exp_spec_rec [lemma, in Stlc.Lemmas]
subst_exp_spec_rec_mutual [lemma, in Stlc.Lemmas]
subst_exp_open_exp_wrt_exp_var [lemma, in Stlc.Lemmas]
subst_exp_open_exp_wrt_exp [lemma, in Stlc.Lemmas]
subst_exp_open_exp_wrt_exp_rec [lemma, in Stlc.Lemmas]
subst_exp_open_exp_wrt_exp_rec_mutual [lemma, in Stlc.Lemmas]
subst_exp_lc_exp [lemma, in Stlc.Lemmas]
subst_exp_fresh [lemma, in Stlc.Lemmas]
subst_exp_fresh_mutual [lemma, in Stlc.Lemmas]
subst_exp_fresh_same [lemma, in Stlc.Lemmas]
subst_exp_fresh_same_mutual [lemma, in Stlc.Lemmas]
subst_exp_fresh_eq [lemma, in Stlc.Lemmas]
subst_exp_fresh_eq_mutual [lemma, in Stlc.Lemmas]
subst_exp_degree_exp_wrt_exp [lemma, in Stlc.Lemmas]
subst_exp_degree_exp_wrt_exp_mutual [lemma, in Stlc.Lemmas]
subst_exp_close_exp_wrt_exp [lemma, in Stlc.Lemmas]
subst_exp_close_exp_wrt_exp_rec [lemma, in Stlc.Lemmas]
subst_exp_close_exp_wrt_exp_rec_mutual [lemma, in Stlc.Lemmas]
swap [definition, in Stlc.Nominal]
swap_spec [lemma, in Stlc.Connect]
swap_spec_aux [lemma, in Stlc.Connect]
swap_size_eq [lemma, in Stlc.Nominal]
swap_equivariance [lemma, in Stlc.Nominal]
swap_var_equivariance [lemma, in Stlc.Nominal]
swap_involutive [lemma, in Stlc.Nominal]
swap_symmetric [lemma, in Stlc.Nominal]
swap_id [lemma, in Stlc.Nominal]
swap_var [definition, in Stlc.Nominal]
swap1 [definition, in Stlc.Nominal]
swap2 [definition, in Stlc.Nominal]
swap3 [definition, in Stlc.Nominal]
T
TakeStep [constructor, in Stlc.Nominal]typ [inductive, in Stlc.Definitions]
typing [inductive, in Stlc.Definitions]
typing_to_lc_exp [lemma, in Stlc.Lec1]
typing_abs_exists [lemma, in Stlc.Lec2]
typing_rename [lemma, in Stlc.Lec2]
typing_uniq [lemma, in Stlc.Lec2]
typing_subst_simple [lemma, in Stlc.Lec2]
typing_subst [lemma, in Stlc.Lec2]
typing_subst_var_case [lemma, in Stlc.Lec2]
typing_weakening [lemma, in Stlc.Lec2]
typing_weakening_strengthened [lemma, in Stlc.Lec2]
typing_weakening_strengthened_1 [lemma, in Stlc.Lec2]
typing_weakening_strengthened_0 [lemma, in Stlc.Lec2]
typing_weakening_0 [lemma, in Stlc.Lec2]
typing_e_app [constructor, in Stlc.Lec2]
typing_e_abs [constructor, in Stlc.Lec2]
typing_e_var [constructor, in Stlc.Lec2]
typing_e [inductive, in Stlc.Lec2]
typing_app [constructor, in Stlc.Definitions]
typing_abs [constructor, in Stlc.Definitions]
typing_var [constructor, in Stlc.Definitions]
typ_arrow [constructor, in Stlc.Definitions]
typ_base [constructor, in Stlc.Definitions]
typ_mutrec [definition, in Stlc.Lemmas]
typ_rec' [definition, in Stlc.Lemmas]
typ_mutind [definition, in Stlc.Lemmas]
typ_ind' [definition, in Stlc.Lemmas]
U
uniq_demo [lemma, in Stlc.Lec2]V
values_are_done [lemma, in Stlc.Nominal]var_f [constructor, in Stlc.Definitions]
var_b [constructor, in Stlc.Definitions]
X
X [definition, in Stlc.Lec1]X [abbreviation, in Stlc.Nominal]
Y
Y [definition, in Stlc.Lec1]Y [abbreviation, in Stlc.Nominal]
Z
Z [definition, in Stlc.Lec1]Z [abbreviation, in Stlc.Nominal]
Notation Index
S
_ ^ _ (exp_scope) [in Stlc.Definitions][ _ ~> _ ] _ (exp_scope) [in Stlc.Definitions]
Module Index
S
StlcNotations [in Stlc.Definitions]Library Index
C
ConnectD
DefinitionsL
Lec1Lec2
Lemmas
N
NominalLemma Index
A
aeq_nom_to_exp [in Stlc.Connect]append_assoc_demo [in Stlc.Lec2]
apply_stack_fresh_eq [in Stlc.Connect]
apply_heap_get [in Stlc.Connect]
apply_stack_cong [in Stlc.Connect]
apply_heap_open [in Stlc.Connect]
apply_heap_app [in Stlc.Connect]
apply_heap_abs [in Stlc.Connect]
apply_heap_lc [in Stlc.Connect]
B
binds_demo [in Stlc.Lec2]C
close_exp_wrt_exp_freshen [in Stlc.Connect]close_exp_wrt_exp_lc_exp [in Stlc.Lemmas]
close_exp_wrt_exp_rec_degree_exp_wrt_exp [in Stlc.Lemmas]
close_exp_wrt_exp_rec_degree_exp_wrt_exp_mutual [in Stlc.Lemmas]
close_exp_wrt_exp_open_exp_wrt_exp [in Stlc.Lemmas]
close_exp_wrt_exp_rec_open_exp_wrt_exp_rec [in Stlc.Lemmas]
close_exp_wrt_exp_rec_open_exp_wrt_exp_rec_mutual [in Stlc.Lemmas]
close_exp_wrt_exp_inj [in Stlc.Lemmas]
close_exp_wrt_exp_rec_inj [in Stlc.Lemmas]
close_exp_wrt_exp_rec_inj_mutual [in Stlc.Lemmas]
cofinite_exists [in Stlc.Lec2]
combine [in Stlc.Connect]
D
decode_lc [in Stlc.Connect]degree_exp_wrt_exp_of_lc_exp [in Stlc.Lemmas]
degree_exp_wrt_exp_of_lc_exp_mutual [in Stlc.Lemmas]
degree_exp_wrt_exp_open_exp_wrt_exp_inv [in Stlc.Lemmas]
degree_exp_wrt_exp_open_exp_wrt_exp_rec_inv [in Stlc.Lemmas]
degree_exp_wrt_exp_open_exp_wrt_exp_rec_inv_mutual [in Stlc.Lemmas]
degree_exp_wrt_exp_open_exp_wrt_exp [in Stlc.Lemmas]
degree_exp_wrt_exp_open_exp_wrt_exp_rec [in Stlc.Lemmas]
degree_exp_wrt_exp_open_exp_wrt_exp_rec_mutual [in Stlc.Lemmas]
degree_exp_wrt_exp_close_exp_wrt_exp_inv [in Stlc.Lemmas]
degree_exp_wrt_exp_close_exp_wrt_exp_rec_inv [in Stlc.Lemmas]
degree_exp_wrt_exp_close_exp_wrt_exp_rec_inv_mutual [in Stlc.Lemmas]
degree_exp_wrt_exp_close_exp_wrt_exp [in Stlc.Lemmas]
degree_exp_wrt_exp_close_exp_wrt_exp_rec [in Stlc.Lemmas]
degree_exp_wrt_exp_close_exp_wrt_exp_rec_mutual [in Stlc.Lemmas]
degree_exp_wrt_exp_O [in Stlc.Lemmas]
degree_exp_wrt_exp_S [in Stlc.Lemmas]
degree_exp_wrt_exp_S_mutual [in Stlc.Lemmas]
demo_lc [in Stlc.Lec1]
demo_open [in Stlc.Lec1]
dom_demo [in Stlc.Lec2]
E
exists_cofinite [in Stlc.Lec2]F
fsetdec_demo [in Stlc.Lec1]fv_exp_open_exp_wrt_exp_upper [in Stlc.Lec1]
fv_exp_subst_exp_upper [in Stlc.Lec1]
fv_exp_subst_exp_fresh [in Stlc.Lec1]
fv_exp_subst_exp_notin [in Stlc.Lec1]
fv_nom_fv_exp_eq [in Stlc.Connect]
fv_in_dom [in Stlc.Lec2]
fv_nom_swap [in Stlc.Nominal]
fv_exp_subst_exp_upper [in Stlc.Lemmas]
fv_exp_subst_exp_upper_mutual [in Stlc.Lemmas]
fv_exp_subst_exp_notin [in Stlc.Lemmas]
fv_exp_subst_exp_notin_mutual [in Stlc.Lemmas]
fv_exp_subst_exp_lower [in Stlc.Lemmas]
fv_exp_subst_exp_lower_mutual [in Stlc.Lemmas]
fv_exp_subst_exp_fresh [in Stlc.Lemmas]
fv_exp_subst_exp_fresh_mutual [in Stlc.Lemmas]
fv_exp_open_exp_wrt_exp_upper [in Stlc.Lemmas]
fv_exp_open_exp_wrt_exp_rec_upper [in Stlc.Lemmas]
fv_exp_open_exp_wrt_exp_rec_upper_mutual [in Stlc.Lemmas]
fv_exp_open_exp_wrt_exp_lower [in Stlc.Lemmas]
fv_exp_open_exp_wrt_exp_rec_lower [in Stlc.Lemmas]
fv_exp_open_exp_wrt_exp_rec_lower_mutual [in Stlc.Lemmas]
fv_exp_close_exp_wrt_exp [in Stlc.Lemmas]
fv_exp_close_exp_wrt_exp_rec [in Stlc.Lemmas]
fv_exp_close_exp_wrt_exp_rec_mutual [in Stlc.Lemmas]
I
in_fv_nom_equivariance [in Stlc.Nominal]L
lc_abs_exists [in Stlc.Lec1]lc_body_abs_1 [in Stlc.Lemmas]
lc_body_exp_wrt_exp [in Stlc.Lemmas]
lc_abs_exists [in Stlc.Lemmas]
lc_exp_of_degree [in Stlc.Lemmas]
lc_exp_of_degree_size_mutual [in Stlc.Lemmas]
M
machine_is_scoped [in Stlc.Connect]N
nom_to_exp_eq_aeq [in Stlc.Connect]nom_to_exp_lc [in Stlc.Connect]
notin_fv_nom_equivariance [in Stlc.Nominal]
O
open_exp_wrt_exp_lc_exp [in Stlc.Lemmas]open_exp_wrt_exp_rec_degree_exp_wrt_exp [in Stlc.Lemmas]
open_exp_wrt_exp_rec_degree_exp_wrt_exp_mutual [in Stlc.Lemmas]
open_exp_wrt_exp_inj [in Stlc.Lemmas]
open_exp_wrt_exp_rec_inj [in Stlc.Lemmas]
open_exp_wrt_exp_rec_inj_mutual [in Stlc.Lemmas]
open_exp_wrt_exp_close_exp_wrt_exp [in Stlc.Lemmas]
open_exp_wrt_exp_rec_close_exp_wrt_exp_rec [in Stlc.Lemmas]
open_exp_wrt_exp_rec_close_exp_wrt_exp_rec_mutual [in Stlc.Lemmas]
P
preservation [in Stlc.Lec2]progress [in Stlc.Lec2]
S
shuffle_swap [in Stlc.Nominal]simpl_env_demo [in Stlc.Lec2]
simulate_error [in Stlc.Connect]
simulate_done [in Stlc.Connect]
simulate_step [in Stlc.Connect]
size_exp_open_exp_wrt_exp_var [in Stlc.Lemmas]
size_exp_open_exp_wrt_exp_rec_var [in Stlc.Lemmas]
size_exp_open_exp_wrt_exp_rec_var_mutual [in Stlc.Lemmas]
size_exp_open_exp_wrt_exp [in Stlc.Lemmas]
size_exp_open_exp_wrt_exp_rec [in Stlc.Lemmas]
size_exp_open_exp_wrt_exp_rec_mutual [in Stlc.Lemmas]
size_exp_close_exp_wrt_exp [in Stlc.Lemmas]
size_exp_close_exp_wrt_exp_rec [in Stlc.Lemmas]
size_exp_close_exp_wrt_exp_rec_mutual [in Stlc.Lemmas]
size_exp_min [in Stlc.Lemmas]
size_exp_min_mutual [in Stlc.Lemmas]
size_typ_min [in Stlc.Lemmas]
size_typ_min_mutual [in Stlc.Lemmas]
step_lc_exp2 [in Stlc.Lec1]
step_lc_exp1 [in Stlc.Lec1]
subst_exp_lc_exp [in Stlc.Lec1]
subst_lc0 [in Stlc.Lec1]
subst_exp_intro [in Stlc.Lec1]
subst_var [in Stlc.Lec1]
subst_exp_open_exp_wrt_exp [in Stlc.Lec1]
subst_exp_fresh_same [in Stlc.Lec1]
subst_exp_fresh_eq [in Stlc.Lec1]
subst_same [in Stlc.Lec1]
subst_neq_var [in Stlc.Lec1]
subst_eq_var [in Stlc.Lec1]
subst_abs [in Stlc.Nominal]
subst_app [in Stlc.Nominal]
subst_neq_var [in Stlc.Nominal]
subst_eq_var [in Stlc.Nominal]
subst_size [in Stlc.Nominal]
subst_exp_intro [in Stlc.Lemmas]
subst_exp_intro_rec [in Stlc.Lemmas]
subst_exp_abs [in Stlc.Lemmas]
subst_exp_close_exp_wrt_exp_open_exp_wrt_exp [in Stlc.Lemmas]
subst_exp_close_exp_wrt_exp_rec_open_exp_wrt_exp_rec [in Stlc.Lemmas]
subst_exp_close_exp_wrt_exp_rec_open_exp_wrt_exp_rec_mutual [in Stlc.Lemmas]
subst_exp_subst_exp [in Stlc.Lemmas]
subst_exp_subst_exp_mutual [in Stlc.Lemmas]
subst_exp_spec [in Stlc.Lemmas]
subst_exp_spec_rec [in Stlc.Lemmas]
subst_exp_spec_rec_mutual [in Stlc.Lemmas]
subst_exp_open_exp_wrt_exp_var [in Stlc.Lemmas]
subst_exp_open_exp_wrt_exp [in Stlc.Lemmas]
subst_exp_open_exp_wrt_exp_rec [in Stlc.Lemmas]
subst_exp_open_exp_wrt_exp_rec_mutual [in Stlc.Lemmas]
subst_exp_lc_exp [in Stlc.Lemmas]
subst_exp_fresh [in Stlc.Lemmas]
subst_exp_fresh_mutual [in Stlc.Lemmas]
subst_exp_fresh_same [in Stlc.Lemmas]
subst_exp_fresh_same_mutual [in Stlc.Lemmas]
subst_exp_fresh_eq [in Stlc.Lemmas]
subst_exp_fresh_eq_mutual [in Stlc.Lemmas]
subst_exp_degree_exp_wrt_exp [in Stlc.Lemmas]
subst_exp_degree_exp_wrt_exp_mutual [in Stlc.Lemmas]
subst_exp_close_exp_wrt_exp [in Stlc.Lemmas]
subst_exp_close_exp_wrt_exp_rec [in Stlc.Lemmas]
subst_exp_close_exp_wrt_exp_rec_mutual [in Stlc.Lemmas]
swap_spec [in Stlc.Connect]
swap_spec_aux [in Stlc.Connect]
swap_size_eq [in Stlc.Nominal]
swap_equivariance [in Stlc.Nominal]
swap_var_equivariance [in Stlc.Nominal]
swap_involutive [in Stlc.Nominal]
swap_symmetric [in Stlc.Nominal]
swap_id [in Stlc.Nominal]
T
typing_to_lc_exp [in Stlc.Lec1]typing_abs_exists [in Stlc.Lec2]
typing_rename [in Stlc.Lec2]
typing_uniq [in Stlc.Lec2]
typing_subst_simple [in Stlc.Lec2]
typing_subst [in Stlc.Lec2]
typing_subst_var_case [in Stlc.Lec2]
typing_weakening [in Stlc.Lec2]
typing_weakening_strengthened [in Stlc.Lec2]
typing_weakening_strengthened_1 [in Stlc.Lec2]
typing_weakening_strengthened_0 [in Stlc.Lec2]
typing_weakening_0 [in Stlc.Lec2]
U
uniq_demo [in Stlc.Lec2]V
values_are_done [in Stlc.Nominal]Constructor Index
A
abs [in Stlc.Definitions]aeq_app [in Stlc.Nominal]
aeq_abs_diff [in Stlc.Nominal]
aeq_abs_same [in Stlc.Nominal]
aeq_var [in Stlc.Nominal]
app [in Stlc.Definitions]
D
degree_wrt_exp_app [in Stlc.Lemmas]degree_wrt_exp_var_b [in Stlc.Lemmas]
degree_wrt_exp_var_f [in Stlc.Lemmas]
degree_wrt_exp_abs [in Stlc.Lemmas]
Done [in Stlc.Nominal]
E
Error [in Stlc.Nominal]L
lc_app [in Stlc.Definitions]lc_abs [in Stlc.Definitions]
lc_var_f [in Stlc.Definitions]
N
n_app2 [in Stlc.Nominal]n_app [in Stlc.Nominal]
n_abs [in Stlc.Nominal]
n_var [in Stlc.Nominal]
S
scoped_conf_witness [in Stlc.Connect]scoped_cons [in Stlc.Connect]
scoped_nil [in Stlc.Connect]
step_app [in Stlc.Definitions]
step_beta [in Stlc.Definitions]
T
TakeStep [in Stlc.Nominal]typing_e_app [in Stlc.Lec2]
typing_e_abs [in Stlc.Lec2]
typing_e_var [in Stlc.Lec2]
typing_app [in Stlc.Definitions]
typing_abs [in Stlc.Definitions]
typing_var [in Stlc.Definitions]
typ_arrow [in Stlc.Definitions]
typ_base [in Stlc.Definitions]
V
var_f [in Stlc.Definitions]var_b [in Stlc.Definitions]
Inductive Index
A
aeq [in Stlc.Nominal]D
degree_exp_wrt_exp [in Stlc.Lemmas]E
exp [in Stlc.Definitions]F
frame [in Stlc.Nominal]L
lc_exp [in Stlc.Definitions]N
n_exp [in Stlc.Nominal]S
scoped_conf [in Stlc.Connect]scoped_heap [in Stlc.Connect]
Step [in Stlc.Nominal]
step [in Stlc.Definitions]
T
typ [in Stlc.Definitions]typing [in Stlc.Definitions]
typing_e [in Stlc.Lec2]
Abbreviation Index
S
stack [in Stlc.Nominal]StlcNotations.open [in Stlc.Definitions]
X
X [in Stlc.Nominal]Y
Y [in Stlc.Nominal]Z
Z [in Stlc.Nominal]Definition Index
A
aeq1 [in Stlc.Nominal]apply_stack [in Stlc.Connect]
apply_heap [in Stlc.Connect]
B
body_exp_wrt_exp [in Stlc.Lemmas]C
close_exp_wrt_exp [in Stlc.Lemmas]close_exp_wrt_exp_rec [in Stlc.Lemmas]
configuration [in Stlc.Nominal]
conf1 [in Stlc.Connect]
ctx [in Stlc.Definitions]
D
decode [in Stlc.Connect]decode1 [in Stlc.Connect]
degree_exp_wrt_exp_mutind [in Stlc.Lemmas]
degree_exp_wrt_exp_ind' [in Stlc.Lemmas]
demo_subst1 [in Stlc.Lec1]
demo_rep3 [in Stlc.Lec1]
demo_rep2 [in Stlc.Lec1]
demo_rep1 [in Stlc.Lec1]
demo_rep2 [in Stlc.Nominal]
demo_rep1 [in Stlc.Nominal]
E
exp_mutrec [in Stlc.Lemmas]exp_rec' [in Stlc.Lemmas]
exp_mutind [in Stlc.Lemmas]
exp_ind' [in Stlc.Lemmas]
F
fv_stack [in Stlc.Connect]fv_nom_rep1 [in Stlc.Nominal]
fv_nom [in Stlc.Nominal]
fv_exp [in Stlc.Definitions]
H
heap [in Stlc.Nominal]I
initconf [in Stlc.Nominal]isVal [in Stlc.Nominal]
is_value [in Stlc.Definitions]
L
lc_exp_mutind [in Stlc.Lemmas]lc_exp_ind' [in Stlc.Lemmas]
M
machine_step [in Stlc.Nominal]N
nom_to_exp [in Stlc.Connect]O
open_exp_wrt_exp [in Stlc.Definitions]open_exp_wrt_exp_rec [in Stlc.Definitions]
S
size [in Stlc.Nominal]size_exp [in Stlc.Lemmas]
size_typ [in Stlc.Lemmas]
subst [in Stlc.Nominal]
subst_rec [in Stlc.Nominal]
subst_exp [in Stlc.Definitions]
swap [in Stlc.Nominal]
swap_var [in Stlc.Nominal]
swap1 [in Stlc.Nominal]
swap2 [in Stlc.Nominal]
swap3 [in Stlc.Nominal]
T
typ_mutrec [in Stlc.Lemmas]typ_rec' [in Stlc.Lemmas]
typ_mutind [in Stlc.Lemmas]
typ_ind' [in Stlc.Lemmas]
X
X [in Stlc.Lec1]Y
Y [in Stlc.Lec1]Z
Z [in Stlc.Lec1]| 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 | (292 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 | (1 entry) |
| 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 | (175 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 | (35 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 | (13 entries) |
| Abbreviation Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (5 entries) |
| 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 | (55 entries) |
This page has been generated by coqdoc