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

Blame


D

Definitions
Desugaring


I

Infrastructure


S

Safety



Lemma 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