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 | (623 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 | (10 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 | (5 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 | (261 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 | (223 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 | (31 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 | (93 entries) |
Global Index
B
Blame [library]blamelabel [definition, in Definitions]
blame_eq_dec [lemma, in Desugaring]
blame_label_ie [definition, in Desugaring]
blame_label_ei [definition, in Desugaring]
blame_label_deref [definition, in Desugaring]
blame_label_op [definition, in Desugaring]
body_itrm_wrt_itrm [definition, in Infrastructure]
body_trm_wrt_trm [definition, in Infrastructure]
C
canonical_forms_arrow [lemma, in Safety]close_pres_safe [lemma, in Desugaring]
close_itrm_wrt_itrm_lc_itrm [lemma, in Infrastructure]
close_trm_wrt_trm_lc_trm [lemma, in Infrastructure]
close_itrm_wrt_itrm_rec_degree_itrm_wrt_itrm [lemma, in Infrastructure]
close_itrm_wrt_itrm_rec_degree_itrm_wrt_itrm_mutual [lemma, in Infrastructure]
close_trm_wrt_trm_rec_degree_trm_wrt_trm [lemma, in Infrastructure]
close_trm_wrt_trm_rec_degree_trm_wrt_trm_mutual [lemma, in Infrastructure]
close_itrm_wrt_itrm_open_itrm_wrt_itrm [lemma, in Infrastructure]
close_trm_wrt_trm_open_trm_wrt_trm [lemma, in Infrastructure]
close_itrm_wrt_itrm_rec_open_itrm_wrt_itrm_rec [lemma, in Infrastructure]
close_itrm_wrt_itrm_rec_open_itrm_wrt_itrm_rec_mutual [lemma, in Infrastructure]
close_trm_wrt_trm_rec_open_trm_wrt_trm_rec [lemma, in Infrastructure]
close_trm_wrt_trm_rec_open_trm_wrt_trm_rec_mutual [lemma, in Infrastructure]
close_itrm_wrt_itrm_inj [lemma, in Infrastructure]
close_trm_wrt_trm_inj [lemma, in Infrastructure]
close_itrm_wrt_itrm_rec_inj [lemma, in Infrastructure]
close_itrm_wrt_itrm_rec_inj_mutual [lemma, in Infrastructure]
close_trm_wrt_trm_rec_inj [lemma, in Infrastructure]
close_trm_wrt_trm_rec_inj_mutual [lemma, in Infrastructure]
close_itrm_wrt_itrm [definition, in Infrastructure]
close_itrm_wrt_itrm_rec [definition, in Infrastructure]
close_trm_wrt_trm [definition, in Infrastructure]
close_trm_wrt_trm_rec [definition, in Infrastructure]
compat [inductive, in Definitions]
compat_typ_ityp [lemma, in Desugaring]
compat_naive_subtyp [lemma, in Desugaring]
compat_arrow [constructor, in Definitions]
compat_null_l [constructor, in Definitions]
compat_null_r [constructor, in Definitions]
compat_base [constructor, in Definitions]
compat_sym [lemma, in Safety]
constant [definition, in Definitions]
ctrm [inductive, in Definitions]
ctrm_of_ictrm [definition, in Desugaring]
ctrm_elvis_blame [definition, in Desugaring]
ctrm_cast [constructor, in Definitions]
ctrm_case_nonnull [constructor, in Definitions]
ctrm_case_null [constructor, in Definitions]
ctrm_case_scrutinee [constructor, in Definitions]
ctrm_lift [constructor, in Definitions]
ctrm_app_right [constructor, in Definitions]
ctrm_app_left [constructor, in Definitions]
ctrm_abs [constructor, in Definitions]
ctrm_binop_right [constructor, in Definitions]
ctrm_binop_left [constructor, in Definitions]
ctrm_hole [constructor, in Definitions]
ctx [definition, in Definitions]
ctx_of_ictx_binds_ityp [lemma, in Desugaring]
ctx_of_ictx [definition, in Desugaring]
ctyping [inductive, in Definitions]
ctyping_cast [constructor, in Definitions]
ctyping_case_nonnull [constructor, in Definitions]
ctyping_case_null [constructor, in Definitions]
ctyping_case_scrutinee [constructor, in Definitions]
ctyping_lift [constructor, in Definitions]
ctyping_app_right [constructor, in Definitions]
ctyping_app_left [constructor, in Definitions]
ctyping_abs [constructor, in Definitions]
ctyping_binop_right [constructor, in Definitions]
ctyping_binop_left [constructor, in Definitions]
ctyping_hole [constructor, in Definitions]
D
Definitions [library]degree_itrm_wrt_itrm_of_lc_itrm [lemma, in Infrastructure]
degree_itrm_wrt_itrm_of_lc_itrm_mutual [lemma, in Infrastructure]
degree_trm_wrt_trm_of_lc_trm [lemma, in Infrastructure]
degree_trm_wrt_trm_of_lc_trm_mutual [lemma, in Infrastructure]
degree_itrm_wrt_itrm_open_itrm_wrt_itrm_inv [lemma, in Infrastructure]
degree_trm_wrt_trm_open_trm_wrt_trm_inv [lemma, in Infrastructure]
degree_itrm_wrt_itrm_open_itrm_wrt_itrm_rec_inv [lemma, in Infrastructure]
degree_itrm_wrt_itrm_open_itrm_wrt_itrm_rec_inv_mutual [lemma, in Infrastructure]
degree_trm_wrt_trm_open_trm_wrt_trm_rec_inv [lemma, in Infrastructure]
degree_trm_wrt_trm_open_trm_wrt_trm_rec_inv_mutual [lemma, in Infrastructure]
degree_itrm_wrt_itrm_open_itrm_wrt_itrm [lemma, in Infrastructure]
degree_trm_wrt_trm_open_trm_wrt_trm [lemma, in Infrastructure]
degree_itrm_wrt_itrm_open_itrm_wrt_itrm_rec [lemma, in Infrastructure]
degree_itrm_wrt_itrm_open_itrm_wrt_itrm_rec_mutual [lemma, in Infrastructure]
degree_trm_wrt_trm_open_trm_wrt_trm_rec [lemma, in Infrastructure]
degree_trm_wrt_trm_open_trm_wrt_trm_rec_mutual [lemma, in Infrastructure]
degree_itrm_wrt_itrm_close_itrm_wrt_itrm_inv [lemma, in Infrastructure]
degree_trm_wrt_trm_close_trm_wrt_trm_inv [lemma, in Infrastructure]
degree_itrm_wrt_itrm_close_itrm_wrt_itrm_rec_inv [lemma, in Infrastructure]
degree_itrm_wrt_itrm_close_itrm_wrt_itrm_rec_inv_mutual [lemma, in Infrastructure]
degree_trm_wrt_trm_close_trm_wrt_trm_rec_inv [lemma, in Infrastructure]
degree_trm_wrt_trm_close_trm_wrt_trm_rec_inv_mutual [lemma, in Infrastructure]
degree_itrm_wrt_itrm_close_itrm_wrt_itrm [lemma, in Infrastructure]
degree_trm_wrt_trm_close_trm_wrt_trm [lemma, in Infrastructure]
degree_itrm_wrt_itrm_close_itrm_wrt_itrm_rec [lemma, in Infrastructure]
degree_itrm_wrt_itrm_close_itrm_wrt_itrm_rec_mutual [lemma, in Infrastructure]
degree_trm_wrt_trm_close_trm_wrt_trm_rec [lemma, in Infrastructure]
degree_trm_wrt_trm_close_trm_wrt_trm_rec_mutual [lemma, in Infrastructure]
degree_itrm_wrt_itrm_O [lemma, in Infrastructure]
degree_trm_wrt_trm_O [lemma, in Infrastructure]
degree_itrm_wrt_itrm_S [lemma, in Infrastructure]
degree_itrm_wrt_itrm_S_mutual [lemma, in Infrastructure]
degree_trm_wrt_trm_S [lemma, in Infrastructure]
degree_trm_wrt_trm_S_mutual [lemma, in Infrastructure]
degree_itrm_wrt_itrm_mutind [definition, in Infrastructure]
degree_itrm_wrt_itrm_ind' [definition, in Infrastructure]
degree_wrt_itrm_itrm_null [constructor, in Infrastructure]
degree_wrt_itrm_itrm_app [constructor, in Infrastructure]
degree_wrt_itrm_itrm_abs [constructor, in Infrastructure]
degree_wrt_itrm_itrm_binop [constructor, in Infrastructure]
degree_wrt_itrm_itrm_const [constructor, in Infrastructure]
degree_wrt_itrm_itrm_var_b [constructor, in Infrastructure]
degree_wrt_itrm_itrm_var_f [constructor, in Infrastructure]
degree_itrm_wrt_itrm [inductive, in Infrastructure]
degree_trm_wrt_trm_mutind [definition, in Infrastructure]
degree_trm_wrt_trm_ind' [definition, in Infrastructure]
degree_wrt_trm_t_blame [constructor, in Infrastructure]
degree_wrt_trm_t_cast [constructor, in Infrastructure]
degree_wrt_trm_t_case [constructor, in Infrastructure]
degree_wrt_trm_t_lift [constructor, in Infrastructure]
degree_wrt_trm_t_null [constructor, in Infrastructure]
degree_wrt_trm_t_app [constructor, in Infrastructure]
degree_wrt_trm_t_abs [constructor, in Infrastructure]
degree_wrt_trm_t_binop [constructor, in Infrastructure]
degree_wrt_trm_t_const [constructor, in Infrastructure]
degree_wrt_trm_t_var_b [constructor, in Infrastructure]
degree_wrt_trm_t_var_f [constructor, in Infrastructure]
degree_trm_wrt_trm [inductive, in Infrastructure]
Desugaring [library]
desugaring_typing [lemma, in Desugaring]
dtyp [inductive, in Definitions]
dtyp_arrow [constructor, in Definitions]
dtyp_base [constructor, in Definitions]
dtyp_rec' [definition, in Infrastructure]
dtyp_ind' [definition, in Infrastructure]
E
elvis [definition, in Desugaring]elvis_blame [definition, in Desugaring]
exp_naive_subtyp [lemma, in Desugaring]
F
fv_ctrm [definition, in Definitions]fv_ictrm [definition, in Definitions]
fv_trm [definition, in Definitions]
fv_itrm [definition, in Definitions]
fv_itrm_subst_itrm_upper [lemma, in Infrastructure]
fv_itrm_subst_itrm_upper_mutual [lemma, in Infrastructure]
fv_trm_subst_trm_upper [lemma, in Infrastructure]
fv_trm_subst_trm_upper_mutual [lemma, in Infrastructure]
fv_itrm_subst_itrm_notin [lemma, in Infrastructure]
fv_itrm_subst_itrm_notin_mutual [lemma, in Infrastructure]
fv_trm_subst_trm_notin [lemma, in Infrastructure]
fv_trm_subst_trm_notin_mutual [lemma, in Infrastructure]
fv_itrm_subst_itrm_lower [lemma, in Infrastructure]
fv_itrm_subst_itrm_lower_mutual [lemma, in Infrastructure]
fv_trm_subst_trm_lower [lemma, in Infrastructure]
fv_trm_subst_trm_lower_mutual [lemma, in Infrastructure]
fv_itrm_subst_itrm_fresh [lemma, in Infrastructure]
fv_itrm_subst_itrm_fresh_mutual [lemma, in Infrastructure]
fv_trm_subst_trm_fresh [lemma, in Infrastructure]
fv_trm_subst_trm_fresh_mutual [lemma, in Infrastructure]
fv_itrm_open_itrm_wrt_itrm_upper [lemma, in Infrastructure]
fv_trm_open_trm_wrt_trm_upper [lemma, in Infrastructure]
fv_itrm_open_itrm_wrt_itrm_rec_upper [lemma, in Infrastructure]
fv_itrm_open_itrm_wrt_itrm_rec_upper_mutual [lemma, in Infrastructure]
fv_trm_open_trm_wrt_trm_rec_upper [lemma, in Infrastructure]
fv_trm_open_trm_wrt_trm_rec_upper_mutual [lemma, in Infrastructure]
fv_itrm_open_itrm_wrt_itrm_lower [lemma, in Infrastructure]
fv_trm_open_trm_wrt_trm_lower [lemma, in Infrastructure]
fv_itrm_open_itrm_wrt_itrm_rec_lower [lemma, in Infrastructure]
fv_itrm_open_itrm_wrt_itrm_rec_lower_mutual [lemma, in Infrastructure]
fv_trm_open_trm_wrt_trm_rec_lower [lemma, in Infrastructure]
fv_trm_open_trm_wrt_trm_rec_lower_mutual [lemma, in Infrastructure]
fv_itrm_close_itrm_wrt_itrm [lemma, in Infrastructure]
fv_trm_close_trm_wrt_trm [lemma, in Infrastructure]
fv_itrm_close_itrm_wrt_itrm_rec [lemma, in Infrastructure]
fv_itrm_close_itrm_wrt_itrm_rec_mutual [lemma, in Infrastructure]
fv_trm_close_trm_wrt_trm_rec [lemma, in Infrastructure]
fv_trm_close_trm_wrt_trm_rec_mutual [lemma, in Infrastructure]
I
ictrm [inductive, in Definitions]ictrm_desugaring_typing [lemma, in Desugaring]
ictrm_app_right [constructor, in Definitions]
ictrm_app_left [constructor, in Definitions]
ictrm_abs [constructor, in Definitions]
ictrm_binop_right [constructor, in Definitions]
ictrm_binop_left [constructor, in Definitions]
ictrm_hole [constructor, in Definitions]
ictx [definition, in Desugaring]
ictx [definition, in Definitions]
ictx_of_ctx [definition, in Desugaring]
ictyping [inductive, in Definitions]
ictyping_app_right [constructor, in Definitions]
ictyping_app_left [constructor, in Definitions]
ictyping_abs [constructor, in Definitions]
ictyping_binop_right [constructor, in Definitions]
ictyping_binop_left [constructor, in Definitions]
ictyping_hole [constructor, in Definitions]
imp_naive_subtyp [lemma, in Desugaring]
Infrastructure [library]
is_val_of_trm [definition, in Definitions]
is_atyp_of_typ [definition, in Definitions]
is_adtyp_of_dtyp [definition, in Definitions]
itrm [inductive, in Definitions]
itrm_null [constructor, in Definitions]
itrm_app [constructor, in Definitions]
itrm_abs [constructor, in Definitions]
itrm_binop [constructor, in Definitions]
itrm_const [constructor, in Definitions]
itrm_var_f [constructor, in Definitions]
itrm_var_b [constructor, in Definitions]
itrm_mutrec [definition, in Infrastructure]
itrm_rec' [definition, in Infrastructure]
itrm_mutind [definition, in Infrastructure]
itrm_ind' [definition, in Infrastructure]
ityp [inductive, in Definitions]
ityping [inductive, in Definitions]
ityping_plugged [lemma, in Desugaring]
ityping_to_lc_itrm [lemma, in Desugaring]
ityping_null [constructor, in Definitions]
ityping_app [constructor, in Definitions]
ityping_abs [constructor, in Definitions]
ityping_binop [constructor, in Definitions]
ityping_base [constructor, in Definitions]
ityping_var [constructor, in Definitions]
ityp_of_typ [definition, in Desugaring]
ityp_arrow [constructor, in Definitions]
ityp_base [constructor, in Definitions]
ityp_mutrec [definition, in Infrastructure]
ityp_rec' [definition, in Infrastructure]
ityp_mutind [definition, in Infrastructure]
ityp_ind' [definition, in Infrastructure]
ivar [definition, in Definitions]
L
label [inductive, in Definitions]label_not_label [constructor, in Definitions]
label_name [constructor, in Definitions]
label_mutrec [definition, in Infrastructure]
label_rec' [definition, in Infrastructure]
label_mutind [definition, in Infrastructure]
label_ind' [definition, in Infrastructure]
lc_ictrm_app_right [constructor, in Definitions]
lc_ictrm_app_left [constructor, in Definitions]
lc_ictrm_abs [constructor, in Definitions]
lc_ictrm_binop_right [constructor, in Definitions]
lc_ictrm_binop_left [constructor, in Definitions]
lc_ictrm_hole [constructor, in Definitions]
lc_ictrm [inductive, in Definitions]
lc_ctrm_cast [constructor, in Definitions]
lc_ctrm_case_nonnull [constructor, in Definitions]
lc_ctrm_case_null [constructor, in Definitions]
lc_ctrm_case_scrutinee [constructor, in Definitions]
lc_ctrm_lift [constructor, in Definitions]
lc_ctrm_app_right [constructor, in Definitions]
lc_ctrm_app_left [constructor, in Definitions]
lc_ctrm_abs [constructor, in Definitions]
lc_ctrm_binop_right [constructor, in Definitions]
lc_ctrm_binop_left [constructor, in Definitions]
lc_ctrm_hole [constructor, in Definitions]
lc_ctrm [inductive, in Definitions]
lc_itrm_null [constructor, in Definitions]
lc_itrm_app [constructor, in Definitions]
lc_itrm_abs [constructor, in Definitions]
lc_itrm_binop [constructor, in Definitions]
lc_itrm_const [constructor, in Definitions]
lc_itrm_var_f [constructor, in Definitions]
lc_itrm [inductive, in Definitions]
lc_t_blame [constructor, in Definitions]
lc_t_cast [constructor, in Definitions]
lc_t_case [constructor, in Definitions]
lc_t_lift [constructor, in Definitions]
lc_t_null [constructor, in Definitions]
lc_t_app [constructor, in Definitions]
lc_t_abs [constructor, in Definitions]
lc_t_binop [constructor, in Definitions]
lc_t_const [constructor, in Definitions]
lc_t_var_f [constructor, in Definitions]
lc_trm [inductive, in Definitions]
lc_set_itrm_of_lc_itrm [lemma, in Infrastructure]
lc_set_itrm_of_lc_itrm_size_mutual [lemma, in Infrastructure]
lc_set_trm_of_lc_trm [lemma, in Infrastructure]
lc_set_trm_of_lc_trm_size_mutual [lemma, in Infrastructure]
lc_itrm_of_lc_set_itrm [lemma, in Infrastructure]
lc_itrm_of_lc_set_itrm_mutual [lemma, in Infrastructure]
lc_trm_of_lc_set_trm [lemma, in Infrastructure]
lc_trm_of_lc_set_trm_mutual [lemma, in Infrastructure]
lc_itrm_unique [lemma, in Infrastructure]
lc_itrm_unique_mutual [lemma, in Infrastructure]
lc_trm_unique [lemma, in Infrastructure]
lc_trm_unique_mutual [lemma, in Infrastructure]
lc_body_itrm_abs_2 [lemma, in Infrastructure]
lc_body_t_case_3 [lemma, in Infrastructure]
lc_body_t_abs_2 [lemma, in Infrastructure]
lc_body_itrm_wrt_itrm [lemma, in Infrastructure]
lc_body_trm_wrt_trm [lemma, in Infrastructure]
lc_itrm_abs_exists [lemma, in Infrastructure]
lc_t_case_exists [lemma, in Infrastructure]
lc_t_abs_exists [lemma, in Infrastructure]
lc_itrm_of_degree [lemma, in Infrastructure]
lc_itrm_of_degree_size_mutual [lemma, in Infrastructure]
lc_trm_of_degree [lemma, in Infrastructure]
lc_trm_of_degree_size_mutual [lemma, in Infrastructure]
lc_set_itrm_mutrec [definition, in Infrastructure]
lc_set_itrm_rec' [definition, in Infrastructure]
lc_set_itrm_mutind [definition, in Infrastructure]
lc_set_itrm_ind' [definition, in Infrastructure]
lc_itrm_mutind [definition, in Infrastructure]
lc_itrm_ind' [definition, in Infrastructure]
lc_set_itrm_null [constructor, in Infrastructure]
lc_set_itrm_app [constructor, in Infrastructure]
lc_set_itrm_abs [constructor, in Infrastructure]
lc_set_itrm_binop [constructor, in Infrastructure]
lc_set_itrm_const [constructor, in Infrastructure]
lc_set_itrm_var_f [constructor, in Infrastructure]
lc_set_itrm [inductive, in Infrastructure]
lc_set_trm_mutrec [definition, in Infrastructure]
lc_set_trm_rec' [definition, in Infrastructure]
lc_set_trm_mutind [definition, in Infrastructure]
lc_set_trm_ind' [definition, in Infrastructure]
lc_trm_mutind [definition, in Infrastructure]
lc_trm_ind' [definition, in Infrastructure]
lc_set_t_blame [constructor, in Infrastructure]
lc_set_t_cast [constructor, in Infrastructure]
lc_set_t_case [constructor, in Infrastructure]
lc_set_t_lift [constructor, in Infrastructure]
lc_set_t_null [constructor, in Infrastructure]
lc_set_t_app [constructor, in Infrastructure]
lc_set_t_abs [constructor, in Infrastructure]
lc_set_t_binop [constructor, in Infrastructure]
lc_set_t_const [constructor, in Infrastructure]
lc_set_t_var_f [constructor, in Infrastructure]
lc_set_trm [inductive, in Infrastructure]
M
multi_step_refl [constructor, in Blame]multi_step [inductive, in Blame]
N
neglabel [inductive, in Definitions]neglabel_not_id [lemma, in Blame]
neglabel_fun_involutive [lemma, in Blame]
neglabel_fun_completeness [lemma, in Blame]
neglabel_fun_completenss [lemma, in Safety]
neglabel_fun_soundness [lemma, in Safety]
neglabel_fun [definition, in Safety]
nest_itrm_in_ctx [lemma, in Desugaring]
nest_trm_in_ictx [lemma, in Desugaring]
nl_neg_to_pos [constructor, in Definitions]
nl_pos_to_neg [constructor, in Definitions]
O
open_ctrm_of_itrm_var [lemma, in Desugaring]open_ctrm_of_itrm_rec_var [lemma, in Desugaring]
open_ctrm_of_ictrm [lemma, in Desugaring]
open_trm_of_itrm_var [lemma, in Desugaring]
open_trm_of_itrm_rec_var [lemma, in Desugaring]
open_trm_of_itrm [lemma, in Desugaring]
open_trm_wrt_trm [definition, in Definitions]
open_itrm_wrt_itrm [definition, in Definitions]
open_ctrm_wrt_trm [definition, in Definitions]
open_ictrm_wrt_itrm [definition, in Definitions]
open_ctrm_wrt_trm_rec [definition, in Definitions]
open_ictrm_wrt_itrm_rec [definition, in Definitions]
open_trm_wrt_trm_rec [definition, in Definitions]
open_itrm_wrt_itrm_rec [definition, in Definitions]
open_itrm_wrt_itrm_lc_itrm [lemma, in Infrastructure]
open_trm_wrt_trm_lc_trm [lemma, in Infrastructure]
open_itrm_wrt_itrm_rec_degree_itrm_wrt_itrm [lemma, in Infrastructure]
open_itrm_wrt_itrm_rec_degree_itrm_wrt_itrm_mutual [lemma, in Infrastructure]
open_trm_wrt_trm_rec_degree_trm_wrt_trm [lemma, in Infrastructure]
open_trm_wrt_trm_rec_degree_trm_wrt_trm_mutual [lemma, in Infrastructure]
open_itrm_wrt_itrm_inj [lemma, in Infrastructure]
open_trm_wrt_trm_inj [lemma, in Infrastructure]
open_itrm_wrt_itrm_rec_inj [lemma, in Infrastructure]
open_itrm_wrt_itrm_rec_inj_mutual [lemma, in Infrastructure]
open_trm_wrt_trm_rec_inj [lemma, in Infrastructure]
open_trm_wrt_trm_rec_inj_mutual [lemma, in Infrastructure]
open_itrm_wrt_itrm_close_itrm_wrt_itrm [lemma, in Infrastructure]
open_trm_wrt_trm_close_trm_wrt_trm [lemma, in Infrastructure]
open_itrm_wrt_itrm_rec_close_itrm_wrt_itrm_rec [lemma, in Infrastructure]
open_itrm_wrt_itrm_rec_close_itrm_wrt_itrm_rec_mutual [lemma, in Infrastructure]
open_trm_wrt_trm_rec_close_trm_wrt_trm_rec [lemma, in Infrastructure]
open_trm_wrt_trm_rec_close_trm_wrt_trm_rec_mutual [lemma, in Infrastructure]
P
plug_ictrm_app_right [constructor, in Desugaring]plug_ictrm_app_left [constructor, in Desugaring]
plug_ictrm_abs [constructor, in Desugaring]
plug_ictrm_binop_right [constructor, in Desugaring]
plug_ictrm_binop_left [constructor, in Desugaring]
plug_ictrm_hole [constructor, in Desugaring]
plug_ictrm [inductive, in Desugaring]
plug_ctrm_cast [constructor, in Desugaring]
plug_ctrm_case_nonnull [constructor, in Desugaring]
plug_ctrm_case_null [constructor, in Desugaring]
plug_ctrm_case_scrutinee [constructor, in Desugaring]
plug_ctrm_lift [constructor, in Desugaring]
plug_ctrm_app_right [constructor, in Desugaring]
plug_ctrm_app_left [constructor, in Desugaring]
plug_ctrm_abs [constructor, in Desugaring]
plug_ctrm_binop_right [constructor, in Desugaring]
plug_ctrm_binop_left [constructor, in Desugaring]
plug_ctrm_hole [constructor, in Desugaring]
plug_ctrm [inductive, in Desugaring]
preservation [lemma, in Safety]
progress [lemma, in Safety]
S
safe [inductive, in Blame]safety [lemma, in Blame]
Safety [library]
safe_progress [lemma, in Blame]
safe_preservation [lemma, in Blame]
safe_blame_diff [constructor, in Blame]
safe_cast_diff [constructor, in Blame]
safe_cast_neg [constructor, in Blame]
safe_cast_pos [constructor, in Blame]
safe_case [constructor, in Blame]
safe_lift [constructor, in Blame]
safe_null [constructor, in Blame]
safe_app [constructor, in Blame]
safe_abs [constructor, in Blame]
safe_binop [constructor, in Blame]
safe_constant [constructor, in Blame]
safe_var [constructor, in Blame]
safe_varb [constructor, in Blame]
size_itrm_open_itrm_wrt_itrm_var [lemma, in Infrastructure]
size_trm_open_trm_wrt_trm_var [lemma, in Infrastructure]
size_itrm_open_itrm_wrt_itrm_rec_var [lemma, in Infrastructure]
size_itrm_open_itrm_wrt_itrm_rec_var_mutual [lemma, in Infrastructure]
size_trm_open_trm_wrt_trm_rec_var [lemma, in Infrastructure]
size_trm_open_trm_wrt_trm_rec_var_mutual [lemma, in Infrastructure]
size_itrm_open_itrm_wrt_itrm [lemma, in Infrastructure]
size_trm_open_trm_wrt_trm [lemma, in Infrastructure]
size_itrm_open_itrm_wrt_itrm_rec [lemma, in Infrastructure]
size_itrm_open_itrm_wrt_itrm_rec_mutual [lemma, in Infrastructure]
size_trm_open_trm_wrt_trm_rec [lemma, in Infrastructure]
size_trm_open_trm_wrt_trm_rec_mutual [lemma, in Infrastructure]
size_itrm_close_itrm_wrt_itrm [lemma, in Infrastructure]
size_trm_close_trm_wrt_trm [lemma, in Infrastructure]
size_itrm_close_itrm_wrt_itrm_rec [lemma, in Infrastructure]
size_itrm_close_itrm_wrt_itrm_rec_mutual [lemma, in Infrastructure]
size_trm_close_trm_wrt_trm_rec [lemma, in Infrastructure]
size_trm_close_trm_wrt_trm_rec_mutual [lemma, in Infrastructure]
size_itrm_min [lemma, in Infrastructure]
size_itrm_min_mutual [lemma, in Infrastructure]
size_ityp_min [lemma, in Infrastructure]
size_ityp_min_mutual [lemma, in Infrastructure]
size_trm_min [lemma, in Infrastructure]
size_trm_min_mutual [lemma, in Infrastructure]
size_label_min [lemma, in Infrastructure]
size_label_min_mutual [lemma, in Infrastructure]
size_dtyp_min [lemma, in Infrastructure]
size_typ_min [lemma, in Infrastructure]
size_typ_min_size_dtyp_min_mutual [lemma, in Infrastructure]
size_itrm [definition, in Infrastructure]
size_ityp [definition, in Infrastructure]
size_trm [definition, in Infrastructure]
size_label [definition, in Infrastructure]
size_dtyp [definition, in Infrastructure]
size_typ [definition, in Infrastructure]
star_step [constructor, in Blame]
step [inductive, in Definitions]
step_binopR_err [constructor, in Definitions]
step_binopR_ctx [constructor, in Definitions]
step_binopL_err [constructor, in Definitions]
step_binopL_ctx [constructor, in Definitions]
step_lift_err [constructor, in Definitions]
step_lift_ctx [constructor, in Definitions]
step_case_err [constructor, in Definitions]
step_case_ctx [constructor, in Definitions]
step_cast_err [constructor, in Definitions]
step_cast_ctx [constructor, in Definitions]
step_appR_err [constructor, in Definitions]
step_appR_ctx [constructor, in Definitions]
step_appL_err [constructor, in Definitions]
step_appL_ctx [constructor, in Definitions]
step_case_lift [constructor, in Definitions]
step_case_null [constructor, in Definitions]
step_cast_base [constructor, in Definitions]
step_upcast [constructor, in Definitions]
step_downcast_lift [constructor, in Definitions]
step_downcast_null [constructor, in Definitions]
step_cast_lift [constructor, in Definitions]
step_cast_null [constructor, in Definitions]
step_wrap [constructor, in Definitions]
step_app [constructor, in Definitions]
step_binop [constructor, in Definitions]
substitution [lemma, in Safety]
substitution_gen [lemma, in Safety]
subst_ctrm [definition, in Definitions]
subst_ictrm [definition, in Definitions]
subst_trm [definition, in Definitions]
subst_itrm [definition, in Definitions]
subst_is_blame [lemma, in Blame]
subst_pres_safe [lemma, in Blame]
subst_itrm_intro [lemma, in Infrastructure]
subst_trm_intro [lemma, in Infrastructure]
subst_itrm_intro_rec [lemma, in Infrastructure]
subst_itrm_intro_rec_mutual [lemma, in Infrastructure]
subst_trm_intro_rec [lemma, in Infrastructure]
subst_trm_intro_rec_mutual [lemma, in Infrastructure]
subst_itrm_itrm_abs [lemma, in Infrastructure]
subst_trm_t_case [lemma, in Infrastructure]
subst_trm_t_abs [lemma, in Infrastructure]
subst_itrm_close_itrm_wrt_itrm_open_itrm_wrt_itrm [lemma, in Infrastructure]
subst_trm_close_trm_wrt_trm_open_trm_wrt_trm [lemma, in Infrastructure]
subst_itrm_close_itrm_wrt_itrm_rec_open_itrm_wrt_itrm_rec [lemma, in Infrastructure]
subst_itrm_close_itrm_wrt_itrm_rec_open_itrm_wrt_itrm_rec_mutual [lemma, in Infrastructure]
subst_trm_close_trm_wrt_trm_rec_open_trm_wrt_trm_rec [lemma, in Infrastructure]
subst_trm_close_trm_wrt_trm_rec_open_trm_wrt_trm_rec_mutual [lemma, in Infrastructure]
subst_itrm_subst_itrm [lemma, in Infrastructure]
subst_itrm_subst_itrm_mutual [lemma, in Infrastructure]
subst_trm_subst_trm [lemma, in Infrastructure]
subst_trm_subst_trm_mutual [lemma, in Infrastructure]
subst_itrm_spec [lemma, in Infrastructure]
subst_trm_spec [lemma, in Infrastructure]
subst_itrm_spec_rec [lemma, in Infrastructure]
subst_itrm_spec_rec_mutual [lemma, in Infrastructure]
subst_trm_spec_rec [lemma, in Infrastructure]
subst_trm_spec_rec_mutual [lemma, in Infrastructure]
subst_itrm_open_itrm_wrt_itrm_var [lemma, in Infrastructure]
subst_trm_open_trm_wrt_trm_var [lemma, in Infrastructure]
subst_itrm_open_itrm_wrt_itrm [lemma, in Infrastructure]
subst_trm_open_trm_wrt_trm [lemma, in Infrastructure]
subst_itrm_open_itrm_wrt_itrm_rec [lemma, in Infrastructure]
subst_itrm_open_itrm_wrt_itrm_rec_mutual [lemma, in Infrastructure]
subst_trm_open_trm_wrt_trm_rec [lemma, in Infrastructure]
subst_trm_open_trm_wrt_trm_rec_mutual [lemma, in Infrastructure]
subst_itrm_lc_itrm [lemma, in Infrastructure]
subst_trm_lc_trm [lemma, in Infrastructure]
subst_itrm_fresh [lemma, in Infrastructure]
subst_itrm_fresh_mutual [lemma, in Infrastructure]
subst_trm_fresh [lemma, in Infrastructure]
subst_trm_fresh_mutual [lemma, in Infrastructure]
subst_itrm_fresh_same [lemma, in Infrastructure]
subst_itrm_fresh_same_mutual [lemma, in Infrastructure]
subst_trm_fresh_same [lemma, in Infrastructure]
subst_trm_fresh_same_mutual [lemma, in Infrastructure]
subst_itrm_fresh_eq [lemma, in Infrastructure]
subst_itrm_fresh_eq_mutual [lemma, in Infrastructure]
subst_trm_fresh_eq [lemma, in Infrastructure]
subst_trm_fresh_eq_mutual [lemma, in Infrastructure]
subst_itrm_degree_itrm_wrt_itrm [lemma, in Infrastructure]
subst_itrm_degree_itrm_wrt_itrm_mutual [lemma, in Infrastructure]
subst_trm_degree_trm_wrt_trm [lemma, in Infrastructure]
subst_trm_degree_trm_wrt_trm_mutual [lemma, in Infrastructure]
subst_itrm_close_itrm_wrt_itrm [lemma, in Infrastructure]
subst_trm_close_trm_wrt_trm [lemma, in Infrastructure]
subst_itrm_close_itrm_wrt_itrm_rec [lemma, in Infrastructure]
subst_itrm_close_itrm_wrt_itrm_rec_mutual [lemma, in Infrastructure]
subst_trm_close_trm_wrt_trm_rec [lemma, in Infrastructure]
subst_trm_close_trm_wrt_trm_rec_mutual [lemma, in Infrastructure]
subtyp [inductive, in Definitions]
subtyp_negarrow [constructor, in Definitions]
subtyp_negnull [constructor, in Definitions]
subtyp_negnull_sup [constructor, in Definitions]
subtyp_negnull_sub [constructor, in Definitions]
subtyp_negbase [constructor, in Definitions]
subtyp_neg [inductive, in Definitions]
subtyp_posarrow [constructor, in Definitions]
subtyp_posnull [constructor, in Definitions]
subtyp_posnull_sup [constructor, in Definitions]
subtyp_posbase [constructor, in Definitions]
subtyp_pos [inductive, in Definitions]
subtyp_n_arrow [constructor, in Definitions]
subtyp_n_null [constructor, in Definitions]
subtyp_n_null_sup [constructor, in Definitions]
subtyp_n_base [constructor, in Definitions]
subtyp_n [inductive, in Definitions]
subtyp_arrow [constructor, in Definitions]
subtyp_null [constructor, in Definitions]
subtyp_null_sup [constructor, in Definitions]
subtyp_base [constructor, in Definitions]
sub_mutind [definition, in Blame]
sub_neg_mut [definition, in Blame]
sub_pos_mut [definition, in Blame]
T
tangram [lemma, in Blame]tangram_naive_rev [lemma, in Blame]
tangram_naive_rev_helper [lemma, in Blame]
tangram_naive_fwd [lemma, in Blame]
tangram_rev [lemma, in Blame]
tangram_rev_helper [lemma, in Blame]
tangram_fwd [lemma, in Blame]
trm [inductive, in Definitions]
trm_of_itrm [definition, in Desugaring]
trm_mutrec [definition, in Infrastructure]
trm_rec' [definition, in Infrastructure]
trm_mutind [definition, in Infrastructure]
trm_ind' [definition, in Infrastructure]
typ [inductive, in Definitions]
typing [inductive, in Definitions]
typing_plugged [lemma, in Desugaring]
typing_blame [constructor, in Definitions]
typing_cast [constructor, in Definitions]
typing_case [constructor, in Definitions]
typing_lift [constructor, in Definitions]
typing_null [constructor, in Definitions]
typing_app [constructor, in Definitions]
typing_abs [constructor, in Definitions]
typing_binop [constructor, in Definitions]
typing_constant [constructor, in Definitions]
typing_var [constructor, in Definitions]
typing_uniq [lemma, in Safety]
typing_to_lc_trm [lemma, in Safety]
typing_weakening [lemma, in Safety]
typ_of_ityp_naive [definition, in Desugaring]
typ_of_ityp [definition, in Desugaring]
typ_null [constructor, in Definitions]
typ_def [constructor, in Definitions]
typ_dtyp_mutrec [definition, in Infrastructure]
typ_rec' [definition, in Infrastructure]
typ_dtyp_mutind [definition, in Infrastructure]
typ_ind' [definition, in Infrastructure]
t_blame [constructor, in Definitions]
t_cast [constructor, in Definitions]
t_case [constructor, in Definitions]
t_lift [constructor, in Definitions]
t_null [constructor, in Definitions]
t_app [constructor, in Definitions]
t_abs [constructor, in Definitions]
t_binop [constructor, in Definitions]
t_const [constructor, in Definitions]
t_var_f [constructor, in Definitions]
t_var_b [constructor, in Definitions]
U
uniq_ctx [lemma, in Desugaring]other
_ ≺n _ [notation, in Blame]_ ≺- _ [notation, in Blame]
_ ≺+ _ [notation, in Blame]
_ ≺ _ [notation, in Blame]
_ ⦂ _ => _ @@ _ [notation, in Safety]
_ ⊢ _ : _ [notation, in Safety]
{{{ _ → _ }}} [notation, in Safety]
~~ _ [notation, in Blame]
λ( _ ) _ [notation, in Safety]
⇑ _ [notation, in Safety]
Notation Index
other
_ ≺n _ [in Blame]_ ≺- _ [in Blame]
_ ≺+ _ [in Blame]
_ ≺ _ [in Blame]
_ ⦂ _ => _ @@ _ [in Safety]
_ ⊢ _ : _ [in Safety]
{{{ _ → _ }}} [in Safety]
~~ _ [in Blame]
λ( _ ) _ [in Safety]
⇑ _ [in Safety]
Library Index
B
BlameD
DefinitionsDesugaring
I
InfrastructureS
SafetyLemma Index
B
blame_eq_dec [in Desugaring]C
canonical_forms_arrow [in Safety]close_pres_safe [in Desugaring]
close_itrm_wrt_itrm_lc_itrm [in Infrastructure]
close_trm_wrt_trm_lc_trm [in Infrastructure]
close_itrm_wrt_itrm_rec_degree_itrm_wrt_itrm [in Infrastructure]
close_itrm_wrt_itrm_rec_degree_itrm_wrt_itrm_mutual [in Infrastructure]
close_trm_wrt_trm_rec_degree_trm_wrt_trm [in Infrastructure]
close_trm_wrt_trm_rec_degree_trm_wrt_trm_mutual [in Infrastructure]
close_itrm_wrt_itrm_open_itrm_wrt_itrm [in Infrastructure]
close_trm_wrt_trm_open_trm_wrt_trm [in Infrastructure]
close_itrm_wrt_itrm_rec_open_itrm_wrt_itrm_rec [in Infrastructure]
close_itrm_wrt_itrm_rec_open_itrm_wrt_itrm_rec_mutual [in Infrastructure]
close_trm_wrt_trm_rec_open_trm_wrt_trm_rec [in Infrastructure]
close_trm_wrt_trm_rec_open_trm_wrt_trm_rec_mutual [in Infrastructure]
close_itrm_wrt_itrm_inj [in Infrastructure]
close_trm_wrt_trm_inj [in Infrastructure]
close_itrm_wrt_itrm_rec_inj [in Infrastructure]
close_itrm_wrt_itrm_rec_inj_mutual [in Infrastructure]
close_trm_wrt_trm_rec_inj [in Infrastructure]
close_trm_wrt_trm_rec_inj_mutual [in Infrastructure]
compat_typ_ityp [in Desugaring]
compat_naive_subtyp [in Desugaring]
compat_sym [in Safety]
ctx_of_ictx_binds_ityp [in Desugaring]
D
degree_itrm_wrt_itrm_of_lc_itrm [in Infrastructure]degree_itrm_wrt_itrm_of_lc_itrm_mutual [in Infrastructure]
degree_trm_wrt_trm_of_lc_trm [in Infrastructure]
degree_trm_wrt_trm_of_lc_trm_mutual [in Infrastructure]
degree_itrm_wrt_itrm_open_itrm_wrt_itrm_inv [in Infrastructure]
degree_trm_wrt_trm_open_trm_wrt_trm_inv [in Infrastructure]
degree_itrm_wrt_itrm_open_itrm_wrt_itrm_rec_inv [in Infrastructure]
degree_itrm_wrt_itrm_open_itrm_wrt_itrm_rec_inv_mutual [in Infrastructure]
degree_trm_wrt_trm_open_trm_wrt_trm_rec_inv [in Infrastructure]
degree_trm_wrt_trm_open_trm_wrt_trm_rec_inv_mutual [in Infrastructure]
degree_itrm_wrt_itrm_open_itrm_wrt_itrm [in Infrastructure]
degree_trm_wrt_trm_open_trm_wrt_trm [in Infrastructure]
degree_itrm_wrt_itrm_open_itrm_wrt_itrm_rec [in Infrastructure]
degree_itrm_wrt_itrm_open_itrm_wrt_itrm_rec_mutual [in Infrastructure]
degree_trm_wrt_trm_open_trm_wrt_trm_rec [in Infrastructure]
degree_trm_wrt_trm_open_trm_wrt_trm_rec_mutual [in Infrastructure]
degree_itrm_wrt_itrm_close_itrm_wrt_itrm_inv [in Infrastructure]
degree_trm_wrt_trm_close_trm_wrt_trm_inv [in Infrastructure]
degree_itrm_wrt_itrm_close_itrm_wrt_itrm_rec_inv [in Infrastructure]
degree_itrm_wrt_itrm_close_itrm_wrt_itrm_rec_inv_mutual [in Infrastructure]
degree_trm_wrt_trm_close_trm_wrt_trm_rec_inv [in Infrastructure]
degree_trm_wrt_trm_close_trm_wrt_trm_rec_inv_mutual [in Infrastructure]
degree_itrm_wrt_itrm_close_itrm_wrt_itrm [in Infrastructure]
degree_trm_wrt_trm_close_trm_wrt_trm [in Infrastructure]
degree_itrm_wrt_itrm_close_itrm_wrt_itrm_rec [in Infrastructure]
degree_itrm_wrt_itrm_close_itrm_wrt_itrm_rec_mutual [in Infrastructure]
degree_trm_wrt_trm_close_trm_wrt_trm_rec [in Infrastructure]
degree_trm_wrt_trm_close_trm_wrt_trm_rec_mutual [in Infrastructure]
degree_itrm_wrt_itrm_O [in Infrastructure]
degree_trm_wrt_trm_O [in Infrastructure]
degree_itrm_wrt_itrm_S [in Infrastructure]
degree_itrm_wrt_itrm_S_mutual [in Infrastructure]
degree_trm_wrt_trm_S [in Infrastructure]
degree_trm_wrt_trm_S_mutual [in Infrastructure]
desugaring_typing [in Desugaring]
E
exp_naive_subtyp [in Desugaring]F
fv_itrm_subst_itrm_upper [in Infrastructure]fv_itrm_subst_itrm_upper_mutual [in Infrastructure]
fv_trm_subst_trm_upper [in Infrastructure]
fv_trm_subst_trm_upper_mutual [in Infrastructure]
fv_itrm_subst_itrm_notin [in Infrastructure]
fv_itrm_subst_itrm_notin_mutual [in Infrastructure]
fv_trm_subst_trm_notin [in Infrastructure]
fv_trm_subst_trm_notin_mutual [in Infrastructure]
fv_itrm_subst_itrm_lower [in Infrastructure]
fv_itrm_subst_itrm_lower_mutual [in Infrastructure]
fv_trm_subst_trm_lower [in Infrastructure]
fv_trm_subst_trm_lower_mutual [in Infrastructure]
fv_itrm_subst_itrm_fresh [in Infrastructure]
fv_itrm_subst_itrm_fresh_mutual [in Infrastructure]
fv_trm_subst_trm_fresh [in Infrastructure]
fv_trm_subst_trm_fresh_mutual [in Infrastructure]
fv_itrm_open_itrm_wrt_itrm_upper [in Infrastructure]
fv_trm_open_trm_wrt_trm_upper [in Infrastructure]
fv_itrm_open_itrm_wrt_itrm_rec_upper [in Infrastructure]
fv_itrm_open_itrm_wrt_itrm_rec_upper_mutual [in Infrastructure]
fv_trm_open_trm_wrt_trm_rec_upper [in Infrastructure]
fv_trm_open_trm_wrt_trm_rec_upper_mutual [in Infrastructure]
fv_itrm_open_itrm_wrt_itrm_lower [in Infrastructure]
fv_trm_open_trm_wrt_trm_lower [in Infrastructure]
fv_itrm_open_itrm_wrt_itrm_rec_lower [in Infrastructure]
fv_itrm_open_itrm_wrt_itrm_rec_lower_mutual [in Infrastructure]
fv_trm_open_trm_wrt_trm_rec_lower [in Infrastructure]
fv_trm_open_trm_wrt_trm_rec_lower_mutual [in Infrastructure]
fv_itrm_close_itrm_wrt_itrm [in Infrastructure]
fv_trm_close_trm_wrt_trm [in Infrastructure]
fv_itrm_close_itrm_wrt_itrm_rec [in Infrastructure]
fv_itrm_close_itrm_wrt_itrm_rec_mutual [in Infrastructure]
fv_trm_close_trm_wrt_trm_rec [in Infrastructure]
fv_trm_close_trm_wrt_trm_rec_mutual [in Infrastructure]
I
ictrm_desugaring_typing [in Desugaring]imp_naive_subtyp [in Desugaring]
ityping_plugged [in Desugaring]
ityping_to_lc_itrm [in Desugaring]
L
lc_set_itrm_of_lc_itrm [in Infrastructure]lc_set_itrm_of_lc_itrm_size_mutual [in Infrastructure]
lc_set_trm_of_lc_trm [in Infrastructure]
lc_set_trm_of_lc_trm_size_mutual [in Infrastructure]
lc_itrm_of_lc_set_itrm [in Infrastructure]
lc_itrm_of_lc_set_itrm_mutual [in Infrastructure]
lc_trm_of_lc_set_trm [in Infrastructure]
lc_trm_of_lc_set_trm_mutual [in Infrastructure]
lc_itrm_unique [in Infrastructure]
lc_itrm_unique_mutual [in Infrastructure]
lc_trm_unique [in Infrastructure]
lc_trm_unique_mutual [in Infrastructure]
lc_body_itrm_abs_2 [in Infrastructure]
lc_body_t_case_3 [in Infrastructure]
lc_body_t_abs_2 [in Infrastructure]
lc_body_itrm_wrt_itrm [in Infrastructure]
lc_body_trm_wrt_trm [in Infrastructure]
lc_itrm_abs_exists [in Infrastructure]
lc_t_case_exists [in Infrastructure]
lc_t_abs_exists [in Infrastructure]
lc_itrm_of_degree [in Infrastructure]
lc_itrm_of_degree_size_mutual [in Infrastructure]
lc_trm_of_degree [in Infrastructure]
lc_trm_of_degree_size_mutual [in Infrastructure]
N
neglabel_not_id [in Blame]neglabel_fun_involutive [in Blame]
neglabel_fun_completeness [in Blame]
neglabel_fun_completenss [in Safety]
neglabel_fun_soundness [in Safety]
nest_itrm_in_ctx [in Desugaring]
nest_trm_in_ictx [in Desugaring]
O
open_ctrm_of_itrm_var [in Desugaring]open_ctrm_of_itrm_rec_var [in Desugaring]
open_ctrm_of_ictrm [in Desugaring]
open_trm_of_itrm_var [in Desugaring]
open_trm_of_itrm_rec_var [in Desugaring]
open_trm_of_itrm [in Desugaring]
open_itrm_wrt_itrm_lc_itrm [in Infrastructure]
open_trm_wrt_trm_lc_trm [in Infrastructure]
open_itrm_wrt_itrm_rec_degree_itrm_wrt_itrm [in Infrastructure]
open_itrm_wrt_itrm_rec_degree_itrm_wrt_itrm_mutual [in Infrastructure]
open_trm_wrt_trm_rec_degree_trm_wrt_trm [in Infrastructure]
open_trm_wrt_trm_rec_degree_trm_wrt_trm_mutual [in Infrastructure]
open_itrm_wrt_itrm_inj [in Infrastructure]
open_trm_wrt_trm_inj [in Infrastructure]
open_itrm_wrt_itrm_rec_inj [in Infrastructure]
open_itrm_wrt_itrm_rec_inj_mutual [in Infrastructure]
open_trm_wrt_trm_rec_inj [in Infrastructure]
open_trm_wrt_trm_rec_inj_mutual [in Infrastructure]
open_itrm_wrt_itrm_close_itrm_wrt_itrm [in Infrastructure]
open_trm_wrt_trm_close_trm_wrt_trm [in Infrastructure]
open_itrm_wrt_itrm_rec_close_itrm_wrt_itrm_rec [in Infrastructure]
open_itrm_wrt_itrm_rec_close_itrm_wrt_itrm_rec_mutual [in Infrastructure]
open_trm_wrt_trm_rec_close_trm_wrt_trm_rec [in Infrastructure]
open_trm_wrt_trm_rec_close_trm_wrt_trm_rec_mutual [in Infrastructure]
P
preservation [in Safety]progress [in Safety]
S
safety [in Blame]safe_progress [in Blame]
safe_preservation [in Blame]
size_itrm_open_itrm_wrt_itrm_var [in Infrastructure]
size_trm_open_trm_wrt_trm_var [in Infrastructure]
size_itrm_open_itrm_wrt_itrm_rec_var [in Infrastructure]
size_itrm_open_itrm_wrt_itrm_rec_var_mutual [in Infrastructure]
size_trm_open_trm_wrt_trm_rec_var [in Infrastructure]
size_trm_open_trm_wrt_trm_rec_var_mutual [in Infrastructure]
size_itrm_open_itrm_wrt_itrm [in Infrastructure]
size_trm_open_trm_wrt_trm [in Infrastructure]
size_itrm_open_itrm_wrt_itrm_rec [in Infrastructure]
size_itrm_open_itrm_wrt_itrm_rec_mutual [in Infrastructure]
size_trm_open_trm_wrt_trm_rec [in Infrastructure]
size_trm_open_trm_wrt_trm_rec_mutual [in Infrastructure]
size_itrm_close_itrm_wrt_itrm [in Infrastructure]
size_trm_close_trm_wrt_trm [in Infrastructure]
size_itrm_close_itrm_wrt_itrm_rec [in Infrastructure]
size_itrm_close_itrm_wrt_itrm_rec_mutual [in Infrastructure]
size_trm_close_trm_wrt_trm_rec [in Infrastructure]
size_trm_close_trm_wrt_trm_rec_mutual [in Infrastructure]
size_itrm_min [in Infrastructure]
size_itrm_min_mutual [in Infrastructure]
size_ityp_min [in Infrastructure]
size_ityp_min_mutual [in Infrastructure]
size_trm_min [in Infrastructure]
size_trm_min_mutual [in Infrastructure]
size_label_min [in Infrastructure]
size_label_min_mutual [in Infrastructure]
size_dtyp_min [in Infrastructure]
size_typ_min [in Infrastructure]
size_typ_min_size_dtyp_min_mutual [in Infrastructure]
substitution [in Safety]
substitution_gen [in Safety]
subst_is_blame [in Blame]
subst_pres_safe [in Blame]
subst_itrm_intro [in Infrastructure]
subst_trm_intro [in Infrastructure]
subst_itrm_intro_rec [in Infrastructure]
subst_itrm_intro_rec_mutual [in Infrastructure]
subst_trm_intro_rec [in Infrastructure]
subst_trm_intro_rec_mutual [in Infrastructure]
subst_itrm_itrm_abs [in Infrastructure]
subst_trm_t_case [in Infrastructure]
subst_trm_t_abs [in Infrastructure]
subst_itrm_close_itrm_wrt_itrm_open_itrm_wrt_itrm [in Infrastructure]
subst_trm_close_trm_wrt_trm_open_trm_wrt_trm [in Infrastructure]
subst_itrm_close_itrm_wrt_itrm_rec_open_itrm_wrt_itrm_rec [in Infrastructure]
subst_itrm_close_itrm_wrt_itrm_rec_open_itrm_wrt_itrm_rec_mutual [in Infrastructure]
subst_trm_close_trm_wrt_trm_rec_open_trm_wrt_trm_rec [in Infrastructure]
subst_trm_close_trm_wrt_trm_rec_open_trm_wrt_trm_rec_mutual [in Infrastructure]
subst_itrm_subst_itrm [in Infrastructure]
subst_itrm_subst_itrm_mutual [in Infrastructure]
subst_trm_subst_trm [in Infrastructure]
subst_trm_subst_trm_mutual [in Infrastructure]
subst_itrm_spec [in Infrastructure]
subst_trm_spec [in Infrastructure]
subst_itrm_spec_rec [in Infrastructure]
subst_itrm_spec_rec_mutual [in Infrastructure]
subst_trm_spec_rec [in Infrastructure]
subst_trm_spec_rec_mutual [in Infrastructure]
subst_itrm_open_itrm_wrt_itrm_var [in Infrastructure]
subst_trm_open_trm_wrt_trm_var [in Infrastructure]
subst_itrm_open_itrm_wrt_itrm [in Infrastructure]
subst_trm_open_trm_wrt_trm [in Infrastructure]
subst_itrm_open_itrm_wrt_itrm_rec [in Infrastructure]
subst_itrm_open_itrm_wrt_itrm_rec_mutual [in Infrastructure]
subst_trm_open_trm_wrt_trm_rec [in Infrastructure]
subst_trm_open_trm_wrt_trm_rec_mutual [in Infrastructure]
subst_itrm_lc_itrm [in Infrastructure]
subst_trm_lc_trm [in Infrastructure]
subst_itrm_fresh [in Infrastructure]
subst_itrm_fresh_mutual [in Infrastructure]
subst_trm_fresh [in Infrastructure]
subst_trm_fresh_mutual [in Infrastructure]
subst_itrm_fresh_same [in Infrastructure]
subst_itrm_fresh_same_mutual [in Infrastructure]
subst_trm_fresh_same [in Infrastructure]
subst_trm_fresh_same_mutual [in Infrastructure]
subst_itrm_fresh_eq [in Infrastructure]
subst_itrm_fresh_eq_mutual [in Infrastructure]
subst_trm_fresh_eq [in Infrastructure]
subst_trm_fresh_eq_mutual [in Infrastructure]
subst_itrm_degree_itrm_wrt_itrm [in Infrastructure]
subst_itrm_degree_itrm_wrt_itrm_mutual [in Infrastructure]
subst_trm_degree_trm_wrt_trm [in Infrastructure]
subst_trm_degree_trm_wrt_trm_mutual [in Infrastructure]
subst_itrm_close_itrm_wrt_itrm [in Infrastructure]
subst_trm_close_trm_wrt_trm [in Infrastructure]
subst_itrm_close_itrm_wrt_itrm_rec [in Infrastructure]
subst_itrm_close_itrm_wrt_itrm_rec_mutual [in Infrastructure]
subst_trm_close_trm_wrt_trm_rec [in Infrastructure]
subst_trm_close_trm_wrt_trm_rec_mutual [in Infrastructure]
T
tangram [in Blame]tangram_naive_rev [in Blame]
tangram_naive_rev_helper [in Blame]
tangram_naive_fwd [in Blame]
tangram_rev [in Blame]
tangram_rev_helper [in Blame]
tangram_fwd [in Blame]
typing_plugged [in Desugaring]
typing_uniq [in Safety]
typing_to_lc_trm [in Safety]
typing_weakening [in Safety]
U
uniq_ctx [in Desugaring]Constructor Index
C
compat_arrow [in Definitions]compat_null_l [in Definitions]
compat_null_r [in Definitions]
compat_base [in Definitions]
ctrm_cast [in Definitions]
ctrm_case_nonnull [in Definitions]
ctrm_case_null [in Definitions]
ctrm_case_scrutinee [in Definitions]
ctrm_lift [in Definitions]
ctrm_app_right [in Definitions]
ctrm_app_left [in Definitions]
ctrm_abs [in Definitions]
ctrm_binop_right [in Definitions]
ctrm_binop_left [in Definitions]
ctrm_hole [in Definitions]
ctyping_cast [in Definitions]
ctyping_case_nonnull [in Definitions]
ctyping_case_null [in Definitions]
ctyping_case_scrutinee [in Definitions]
ctyping_lift [in Definitions]
ctyping_app_right [in Definitions]
ctyping_app_left [in Definitions]
ctyping_abs [in Definitions]
ctyping_binop_right [in Definitions]
ctyping_binop_left [in Definitions]
ctyping_hole [in Definitions]
D
degree_wrt_itrm_itrm_null [in Infrastructure]degree_wrt_itrm_itrm_app [in Infrastructure]
degree_wrt_itrm_itrm_abs [in Infrastructure]
degree_wrt_itrm_itrm_binop [in Infrastructure]
degree_wrt_itrm_itrm_const [in Infrastructure]
degree_wrt_itrm_itrm_var_b [in Infrastructure]
degree_wrt_itrm_itrm_var_f [in Infrastructure]
degree_wrt_trm_t_blame [in Infrastructure]
degree_wrt_trm_t_cast [in Infrastructure]
degree_wrt_trm_t_case [in Infrastructure]
degree_wrt_trm_t_lift [in Infrastructure]
degree_wrt_trm_t_null [in Infrastructure]
degree_wrt_trm_t_app [in Infrastructure]
degree_wrt_trm_t_abs [in Infrastructure]
degree_wrt_trm_t_binop [in Infrastructure]
degree_wrt_trm_t_const [in Infrastructure]
degree_wrt_trm_t_var_b [in Infrastructure]
degree_wrt_trm_t_var_f [in Infrastructure]
dtyp_arrow [in Definitions]
dtyp_base [in Definitions]
I
ictrm_app_right [in Definitions]ictrm_app_left [in Definitions]
ictrm_abs [in Definitions]
ictrm_binop_right [in Definitions]
ictrm_binop_left [in Definitions]
ictrm_hole [in Definitions]
ictyping_app_right [in Definitions]
ictyping_app_left [in Definitions]
ictyping_abs [in Definitions]
ictyping_binop_right [in Definitions]
ictyping_binop_left [in Definitions]
ictyping_hole [in Definitions]
itrm_null [in Definitions]
itrm_app [in Definitions]
itrm_abs [in Definitions]
itrm_binop [in Definitions]
itrm_const [in Definitions]
itrm_var_f [in Definitions]
itrm_var_b [in Definitions]
ityping_null [in Definitions]
ityping_app [in Definitions]
ityping_abs [in Definitions]
ityping_binop [in Definitions]
ityping_base [in Definitions]
ityping_var [in Definitions]
ityp_arrow [in Definitions]
ityp_base [in Definitions]
L
label_not_label [in Definitions]label_name [in Definitions]
lc_ictrm_app_right [in Definitions]
lc_ictrm_app_left [in Definitions]
lc_ictrm_abs [in Definitions]
lc_ictrm_binop_right [in Definitions]
lc_ictrm_binop_left [in Definitions]
lc_ictrm_hole [in Definitions]
lc_ctrm_cast [in Definitions]
lc_ctrm_case_nonnull [in Definitions]
lc_ctrm_case_null [in Definitions]
lc_ctrm_case_scrutinee [in Definitions]
lc_ctrm_lift [in Definitions]
lc_ctrm_app_right [in Definitions]
lc_ctrm_app_left [in Definitions]
lc_ctrm_abs [in Definitions]
lc_ctrm_binop_right [in Definitions]
lc_ctrm_binop_left [in Definitions]
lc_ctrm_hole [in Definitions]
lc_itrm_null [in Definitions]
lc_itrm_app [in Definitions]
lc_itrm_abs [in Definitions]
lc_itrm_binop [in Definitions]
lc_itrm_const [in Definitions]
lc_itrm_var_f [in Definitions]
lc_t_blame [in Definitions]
lc_t_cast [in Definitions]
lc_t_case [in Definitions]
lc_t_lift [in Definitions]
lc_t_null [in Definitions]
lc_t_app [in Definitions]
lc_t_abs [in Definitions]
lc_t_binop [in Definitions]
lc_t_const [in Definitions]
lc_t_var_f [in Definitions]
lc_set_itrm_null [in Infrastructure]
lc_set_itrm_app [in Infrastructure]
lc_set_itrm_abs [in Infrastructure]
lc_set_itrm_binop [in Infrastructure]
lc_set_itrm_const [in Infrastructure]
lc_set_itrm_var_f [in Infrastructure]
lc_set_t_blame [in Infrastructure]
lc_set_t_cast [in Infrastructure]
lc_set_t_case [in Infrastructure]
lc_set_t_lift [in Infrastructure]
lc_set_t_null [in Infrastructure]
lc_set_t_app [in Infrastructure]
lc_set_t_abs [in Infrastructure]
lc_set_t_binop [in Infrastructure]
lc_set_t_const [in Infrastructure]
lc_set_t_var_f [in Infrastructure]
M
multi_step_refl [in Blame]N
nl_neg_to_pos [in Definitions]nl_pos_to_neg [in Definitions]
P
plug_ictrm_app_right [in Desugaring]plug_ictrm_app_left [in Desugaring]
plug_ictrm_abs [in Desugaring]
plug_ictrm_binop_right [in Desugaring]
plug_ictrm_binop_left [in Desugaring]
plug_ictrm_hole [in Desugaring]
plug_ctrm_cast [in Desugaring]
plug_ctrm_case_nonnull [in Desugaring]
plug_ctrm_case_null [in Desugaring]
plug_ctrm_case_scrutinee [in Desugaring]
plug_ctrm_lift [in Desugaring]
plug_ctrm_app_right [in Desugaring]
plug_ctrm_app_left [in Desugaring]
plug_ctrm_abs [in Desugaring]
plug_ctrm_binop_right [in Desugaring]
plug_ctrm_binop_left [in Desugaring]
plug_ctrm_hole [in Desugaring]
S
safe_blame_diff [in Blame]safe_cast_diff [in Blame]
safe_cast_neg [in Blame]
safe_cast_pos [in Blame]
safe_case [in Blame]
safe_lift [in Blame]
safe_null [in Blame]
safe_app [in Blame]
safe_abs [in Blame]
safe_binop [in Blame]
safe_constant [in Blame]
safe_var [in Blame]
safe_varb [in Blame]
star_step [in Blame]
step_binopR_err [in Definitions]
step_binopR_ctx [in Definitions]
step_binopL_err [in Definitions]
step_binopL_ctx [in Definitions]
step_lift_err [in Definitions]
step_lift_ctx [in Definitions]
step_case_err [in Definitions]
step_case_ctx [in Definitions]
step_cast_err [in Definitions]
step_cast_ctx [in Definitions]
step_appR_err [in Definitions]
step_appR_ctx [in Definitions]
step_appL_err [in Definitions]
step_appL_ctx [in Definitions]
step_case_lift [in Definitions]
step_case_null [in Definitions]
step_cast_base [in Definitions]
step_upcast [in Definitions]
step_downcast_lift [in Definitions]
step_downcast_null [in Definitions]
step_cast_lift [in Definitions]
step_cast_null [in Definitions]
step_wrap [in Definitions]
step_app [in Definitions]
step_binop [in Definitions]
subtyp_negarrow [in Definitions]
subtyp_negnull [in Definitions]
subtyp_negnull_sup [in Definitions]
subtyp_negnull_sub [in Definitions]
subtyp_negbase [in Definitions]
subtyp_posarrow [in Definitions]
subtyp_posnull [in Definitions]
subtyp_posnull_sup [in Definitions]
subtyp_posbase [in Definitions]
subtyp_n_arrow [in Definitions]
subtyp_n_null [in Definitions]
subtyp_n_null_sup [in Definitions]
subtyp_n_base [in Definitions]
subtyp_arrow [in Definitions]
subtyp_null [in Definitions]
subtyp_null_sup [in Definitions]
subtyp_base [in Definitions]
T
typing_blame [in Definitions]typing_cast [in Definitions]
typing_case [in Definitions]
typing_lift [in Definitions]
typing_null [in Definitions]
typing_app [in Definitions]
typing_abs [in Definitions]
typing_binop [in Definitions]
typing_constant [in Definitions]
typing_var [in Definitions]
typ_null [in Definitions]
typ_def [in Definitions]
t_blame [in Definitions]
t_cast [in Definitions]
t_case [in Definitions]
t_lift [in Definitions]
t_null [in Definitions]
t_app [in Definitions]
t_abs [in Definitions]
t_binop [in Definitions]
t_const [in Definitions]
t_var_f [in Definitions]
t_var_b [in Definitions]
Inductive Index
C
compat [in Definitions]ctrm [in Definitions]
ctyping [in Definitions]
D
degree_itrm_wrt_itrm [in Infrastructure]degree_trm_wrt_trm [in Infrastructure]
dtyp [in Definitions]
I
ictrm [in Definitions]ictyping [in Definitions]
itrm [in Definitions]
ityp [in Definitions]
ityping [in Definitions]
L
label [in Definitions]lc_ictrm [in Definitions]
lc_ctrm [in Definitions]
lc_itrm [in Definitions]
lc_trm [in Definitions]
lc_set_itrm [in Infrastructure]
lc_set_trm [in Infrastructure]
M
multi_step [in Blame]N
neglabel [in Definitions]P
plug_ictrm [in Desugaring]plug_ctrm [in Desugaring]
S
safe [in Blame]step [in Definitions]
subtyp [in Definitions]
subtyp_neg [in Definitions]
subtyp_pos [in Definitions]
subtyp_n [in Definitions]
T
trm [in Definitions]typ [in Definitions]
typing [in Definitions]
Definition Index
B
blamelabel [in Definitions]blame_label_ie [in Desugaring]
blame_label_ei [in Desugaring]
blame_label_deref [in Desugaring]
blame_label_op [in Desugaring]
body_itrm_wrt_itrm [in Infrastructure]
body_trm_wrt_trm [in Infrastructure]
C
close_itrm_wrt_itrm [in Infrastructure]close_itrm_wrt_itrm_rec [in Infrastructure]
close_trm_wrt_trm [in Infrastructure]
close_trm_wrt_trm_rec [in Infrastructure]
constant [in Definitions]
ctrm_of_ictrm [in Desugaring]
ctrm_elvis_blame [in Desugaring]
ctx [in Definitions]
ctx_of_ictx [in Desugaring]
D
degree_itrm_wrt_itrm_mutind [in Infrastructure]degree_itrm_wrt_itrm_ind' [in Infrastructure]
degree_trm_wrt_trm_mutind [in Infrastructure]
degree_trm_wrt_trm_ind' [in Infrastructure]
dtyp_rec' [in Infrastructure]
dtyp_ind' [in Infrastructure]
E
elvis [in Desugaring]elvis_blame [in Desugaring]
F
fv_ctrm [in Definitions]fv_ictrm [in Definitions]
fv_trm [in Definitions]
fv_itrm [in Definitions]
I
ictx [in Desugaring]ictx [in Definitions]
ictx_of_ctx [in Desugaring]
is_val_of_trm [in Definitions]
is_atyp_of_typ [in Definitions]
is_adtyp_of_dtyp [in Definitions]
itrm_mutrec [in Infrastructure]
itrm_rec' [in Infrastructure]
itrm_mutind [in Infrastructure]
itrm_ind' [in Infrastructure]
ityp_of_typ [in Desugaring]
ityp_mutrec [in Infrastructure]
ityp_rec' [in Infrastructure]
ityp_mutind [in Infrastructure]
ityp_ind' [in Infrastructure]
ivar [in Definitions]
L
label_mutrec [in Infrastructure]label_rec' [in Infrastructure]
label_mutind [in Infrastructure]
label_ind' [in Infrastructure]
lc_set_itrm_mutrec [in Infrastructure]
lc_set_itrm_rec' [in Infrastructure]
lc_set_itrm_mutind [in Infrastructure]
lc_set_itrm_ind' [in Infrastructure]
lc_itrm_mutind [in Infrastructure]
lc_itrm_ind' [in Infrastructure]
lc_set_trm_mutrec [in Infrastructure]
lc_set_trm_rec' [in Infrastructure]
lc_set_trm_mutind [in Infrastructure]
lc_set_trm_ind' [in Infrastructure]
lc_trm_mutind [in Infrastructure]
lc_trm_ind' [in Infrastructure]
N
neglabel_fun [in Safety]O
open_trm_wrt_trm [in Definitions]open_itrm_wrt_itrm [in Definitions]
open_ctrm_wrt_trm [in Definitions]
open_ictrm_wrt_itrm [in Definitions]
open_ctrm_wrt_trm_rec [in Definitions]
open_ictrm_wrt_itrm_rec [in Definitions]
open_trm_wrt_trm_rec [in Definitions]
open_itrm_wrt_itrm_rec [in Definitions]
S
size_itrm [in Infrastructure]size_ityp [in Infrastructure]
size_trm [in Infrastructure]
size_label [in Infrastructure]
size_dtyp [in Infrastructure]
size_typ [in Infrastructure]
subst_ctrm [in Definitions]
subst_ictrm [in Definitions]
subst_trm [in Definitions]
subst_itrm [in Definitions]
sub_mutind [in Blame]
sub_neg_mut [in Blame]
sub_pos_mut [in Blame]
T
trm_of_itrm [in Desugaring]trm_mutrec [in Infrastructure]
trm_rec' [in Infrastructure]
trm_mutind [in Infrastructure]
trm_ind' [in Infrastructure]
typ_of_ityp_naive [in Desugaring]
typ_of_ityp [in Desugaring]
typ_dtyp_mutrec [in Infrastructure]
typ_rec' [in Infrastructure]
typ_dtyp_mutind [in Infrastructure]
typ_ind' [in Infrastructure]
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 | (623 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 | (10 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 | (5 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 | (261 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 | (223 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 | (31 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 | (93 entries) |
This page has been generated by coqdoc