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 (331 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 (13 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 (14 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 (99 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 (114 entries)
Axiom Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ other (2 entries)
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 (28 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 (61 entries)

Global Index

A

avar [inductive, in Definitions]
avar_f [constructor, in Definitions]
avar_b [constructor, in Definitions]


B

Binding [library]
binds_inert [lemma, in PreciseTyping]


C

CanonicalForms [library]
canonical_forms_obj [lemma, in CanonicalForms]
canonical_forms_fun [lemma, in CanonicalForms]
corresponding_types [lemma, in CanonicalForms]
ctx [definition, in Definitions]


D

dec [inductive, in Definitions]
dec_mut [definition, in Definitions]
dec_trm [constructor, in Definitions]
dec_typ [constructor, in Definitions]
def [inductive, in Definitions]
Definitions [library]
defs [inductive, in Definitions]
defs_has_hasnt_neq [lemma, in CanonicalForms]
defs_has_inv [lemma, in RecordAndInertTypes]
defs_mut [definition, in Definitions]
defs_hasnt [definition, in Definitions]
defs_has [definition, in Definitions]
defs_cons [constructor, in Definitions]
defs_nil [constructor, in Definitions]
def_mut [definition, in Definitions]
def_trm [constructor, in Definitions]
def_typ [constructor, in Definitions]


F

fv_ctx_types_push_eq [lemma, in Binding]
fv_sta_vals [definition, in Definitions]
fv_ctx_types [definition, in Definitions]
fv_defs [definition, in Definitions]
fv_def [definition, in Definitions]
fv_val [definition, in Definitions]
fv_trm [definition, in Definitions]
fv_dec [definition, in Definitions]
fv_typ [definition, in Definitions]
fv_avar [definition, in Definitions]


G

GeneralToTight [library]
general_to_tight_typing [lemma, in GeneralToTight]
general_to_tight [lemma, in GeneralToTight]
get_def [definition, in Definitions]


H

hasnt_notin [lemma, in RecordAndInertTypes]


I

inert [inductive, in RecordAndInertTypes]
inert_concat [lemma, in RecordAndInertTypes]
inert_all [constructor, in RecordAndInertTypes]
inert_empty [constructor, in RecordAndInertTypes]
inert_typ_bnd [constructor, in RecordAndInertTypes]
inert_typ_all [constructor, in RecordAndInertTypes]
inert_typ [inductive, in RecordAndInertTypes]
inert_ok [lemma, in PreciseTyping]
inert_precise_all_inv [lemma, in PreciseTyping]
InvertibleTyping [library]
invertible_val_to_precise_lambda [lemma, in CanonicalForms]
invertible_typing_closure_tight_v [lemma, in InvertibleTyping]
invertible_typing_closure_tight [lemma, in InvertibleTyping]
invertible_to_precise_typ_all [lemma, in InvertibleTyping]
invertible_to_precise_trm_dec [lemma, in InvertibleTyping]
invert_fv_ctx_types_push [lemma, in Binding]


L

label [inductive, in Definitions]
label_of_dec [definition, in Definitions]
label_of_def [definition, in Definitions]
label_trm [constructor, in Definitions]
label_typ [constructor, in Definitions]


N

Narrowing [library]
narrow_subtyping [lemma, in Narrowing]
narrow_typing [lemma, in Narrowing]
narrow_rules [lemma, in Narrowing]
nf_val [constructor, in OperationalSemantics]
nf_var [constructor, in OperationalSemantics]
norm_form [inductive, in OperationalSemantics]


O

opening_preserves_labels [lemma, in RecordAndInertTypes]
open_fresh_typ_dec_injective [lemma, in Binding]
open_fresh_avar_injective [lemma, in Binding]
open_record_type [lemma, in RecordAndInertTypes]
open_record_typ [lemma, in RecordAndInertTypes]
open_record_dec [lemma, in RecordAndInertTypes]
open_dec_preserves_label [lemma, in RecordAndInertTypes]
open_defs [definition, in Definitions]
open_def [definition, in Definitions]
open_val [definition, in Definitions]
open_trm [definition, in Definitions]
open_dec [definition, in Definitions]
open_typ [definition, in Definitions]
open_avar [definition, in Definitions]
open_rec_defs [definition, in Definitions]
open_rec_def [definition, in Definitions]
open_rec_val [definition, in Definitions]
open_rec_trm [definition, in Definitions]
open_rec_dec [definition, in Definitions]
open_rec_typ [definition, in Definitions]
open_rec_avar [definition, in Definitions]
OperationalSemantics [library]


P

pf_dec_typ_inv [lemma, in PreciseTyping]
pf_inert_unique_tight_bounds [lemma, in PreciseTyping]
pf_record_unique_tight_bounds_rec [lemma, in PreciseTyping]
pf_record_sub [lemma, in PreciseTyping]
pf_psel_false [lemma, in PreciseTyping]
pf_bot_false [lemma, in PreciseTyping]
pf_inert_lambda_U [lemma, in PreciseTyping]
pf_inert_rcd_typ_U [lemma, in PreciseTyping]
pf_inert_rcd_U [lemma, in PreciseTyping]
pf_inert_bnd_U [lemma, in PreciseTyping]
pf_bnd_same_or_rcd [lemma, in PreciseTyping]
pf_rcd_T [lemma, in PreciseTyping]
pf_inert_T [lemma, in PreciseTyping]
pf_binds [lemma, in PreciseTyping]
pf_and2 [constructor, in PreciseTyping]
pf_and1 [constructor, in PreciseTyping]
pf_open [constructor, in PreciseTyping]
pf_bind [constructor, in PreciseTyping]
PreciseTyping [library]
precise_to_general_v [lemma, in PreciseTyping]
precise_to_general [lemma, in PreciseTyping]
precise_flow_record_has [lemma, in PreciseTyping]
precise_inert_typ [lemma, in PreciseTyping]
precise_flow_all_inv [lemma, in PreciseTyping]
precise_flow [inductive, in PreciseTyping]
preservation [lemma, in Safety]
preservation_helper [lemma, in Safety]
progress [lemma, in Safety]


R

rd_trm [constructor, in RecordAndInertTypes]
rd_typ [constructor, in RecordAndInertTypes]
RecordAndInertTypes [library]
record_has_ty_defs [lemma, in CanonicalForms]
record_typ_has_label_in [lemma, in RecordAndInertTypes]
record_type_open [lemma, in RecordAndInertTypes]
record_has [inductive, in RecordAndInertTypes]
record_type [definition, in RecordAndInertTypes]
record_typ [inductive, in RecordAndInertTypes]
record_dec [inductive, in RecordAndInertTypes]
red [inductive, in OperationalSemantics]
red_let_tgt [constructor, in OperationalSemantics]
red_let_var [constructor, in OperationalSemantics]
red_let_val [constructor, in OperationalSemantics]
red_app [constructor, in OperationalSemantics]
red_sel [constructor, in OperationalSemantics]
renaming_fresh [lemma, in Substitution]
renaming_typ [lemma, in Substitution]
renaming_def [lemma, in Substitution]
rh_andr [constructor, in RecordAndInertTypes]
rh_andl [constructor, in RecordAndInertTypes]
rh_one [constructor, in RecordAndInertTypes]
rt_cons [constructor, in RecordAndInertTypes]
rt_one [constructor, in RecordAndInertTypes]
rules_mutind [definition, in Definitions]
rules_subtyp [definition, in Definitions]
rules_defs_mut [definition, in Definitions]
rules_def_mut [definition, in Definitions]
rules_trm_mut [definition, in Definitions]


S

Safety [library]
sel_replacement [lemma, in GeneralToTight]
sel_premise [lemma, in GeneralToTight]
sta [definition, in Definitions]
sta_trm_typ_c [constructor, in Safety]
sta_trm_typ [inductive, in Safety]
subenv [inductive, in Subenvironments]
Subenvironments [library]
subenv_implies_ok [lemma, in Subenvironments]
subenv_last [lemma, in Subenvironments]
subenv_push [lemma, in Subenvironments]
subenv_refl [lemma, in Subenvironments]
subenv_grow [constructor, in Subenvironments]
subenv_empty [constructor, in Subenvironments]
Substitution [library]
subst_ty_defs [lemma, in Substitution]
subst_ty_trm [lemma, in Substitution]
subst_rules [lemma, in Substitution]
subst_defs_hasnt [lemma, in Binding]
subst_label_of_def [lemma, in Binding]
subst_intro_typ [lemma, in Binding]
subst_intro_defs [lemma, in Binding]
subst_intro_trm [lemma, in Binding]
subst_open_commut_defs [lemma, in Binding]
subst_open_commut_trm [lemma, in Binding]
subst_open_commut_trm_val_def_defs [lemma, in Binding]
subst_open_commut_typ [lemma, in Binding]
subst_open_commut_typ_dec [lemma, in Binding]
subst_open_commut_avar [lemma, in Binding]
subst_fvar [definition, in Binding]
subst_fresh_ctx [lemma, in Binding]
subst_fresh_trm_val_def_defs [lemma, in Binding]
subst_fresh_typ [definition, in Binding]
subst_fresh_typ_dec [lemma, in Binding]
subst_fresh_avar [lemma, in Binding]
subst_env [definition, in Binding]
subst_ctx [definition, in Binding]
subst_defs [definition, in Binding]
subst_def [definition, in Binding]
subst_val [definition, in Binding]
subst_trm [definition, in Binding]
subst_dec [definition, in Binding]
subst_typ [definition, in Binding]
subst_avar [definition, in Binding]
subtyp [inductive, in Definitions]
subtyp_all_t [constructor, in TightTyping]
subtyp_sel1_t [constructor, in TightTyping]
subtyp_sel2_t [constructor, in TightTyping]
subtyp_typ_t [constructor, in TightTyping]
subtyp_fld_t [constructor, in TightTyping]
subtyp_and2_t [constructor, in TightTyping]
subtyp_and12_t [constructor, in TightTyping]
subtyp_and11_t [constructor, in TightTyping]
subtyp_trans_t [constructor, in TightTyping]
subtyp_refl_t [constructor, in TightTyping]
subtyp_bot_t [constructor, in TightTyping]
subtyp_top_t [constructor, in TightTyping]
subtyp_t [inductive, in TightTyping]
subtyp_all [constructor, in Definitions]
subtyp_sel1 [constructor, in Definitions]
subtyp_sel2 [constructor, in Definitions]
subtyp_typ [constructor, in Definitions]
subtyp_fld [constructor, in Definitions]
subtyp_and2 [constructor, in Definitions]
subtyp_and12 [constructor, in Definitions]
subtyp_and11 [constructor, in Definitions]
subtyp_trans [constructor, in Definitions]
subtyp_refl [constructor, in Definitions]
subtyp_bot [constructor, in Definitions]
subtyp_top [constructor, in Definitions]


T

TightTyping [library]
tight_to_general [lemma, in TightTyping]
tight_to_invertible_v [lemma, in InvertibleTyping]
tight_to_invertible [lemma, in InvertibleTyping]
trm [inductive, in Definitions]
trm_mutind [definition, in Definitions]
trm_mut [definition, in Definitions]
trm_let [constructor, in Definitions]
trm_app [constructor, in Definitions]
trm_sel [constructor, in Definitions]
trm_val [constructor, in Definitions]
trm_var [constructor, in Definitions]
trm_label [axiom, in Definitions]
ts_t_mutind [definition, in TightTyping]
ts_subtyp_t [definition, in TightTyping]
ts_ty_trm_t_mut [definition, in TightTyping]
ts_mutind [definition, in Definitions]
ts_subtyp [definition, in Definitions]
ts_ty_trm_mut [definition, in Definitions]
typ [inductive, in Definitions]
typing_implies_bound [lemma, in CanonicalForms]
typ_mutind [definition, in Definitions]
typ_mut [definition, in Definitions]
typ_all [constructor, in Definitions]
typ_bnd [constructor, in Definitions]
typ_sel [constructor, in Definitions]
typ_and [constructor, in Definitions]
typ_rcd [constructor, in Definitions]
typ_bot [constructor, in Definitions]
typ_top [constructor, in Definitions]
typ_label [axiom, in Definitions]
ty_sub_t [constructor, in TightTyping]
ty_and_intro_t [constructor, in TightTyping]
ty_rec_elim_t [constructor, in TightTyping]
ty_rec_intro_t [constructor, in TightTyping]
ty_let_t [constructor, in TightTyping]
ty_new_elim_t [constructor, in TightTyping]
ty_new_intro_t [constructor, in TightTyping]
ty_all_elim_t [constructor, in TightTyping]
ty_all_intro_t [constructor, in TightTyping]
ty_var_t [constructor, in TightTyping]
ty_trm_t [inductive, in TightTyping]
ty_defs_record_type [lemma, in RecordAndInertTypes]
ty_defs_cons [constructor, in Definitions]
ty_defs_one [constructor, in Definitions]
ty_defs [inductive, in Definitions]
ty_def_trm [constructor, in Definitions]
ty_def_typ [constructor, in Definitions]
ty_def [inductive, in Definitions]
ty_sub [constructor, in Definitions]
ty_and_intro [constructor, in Definitions]
ty_rec_elim [constructor, in Definitions]
ty_rec_intro [constructor, in Definitions]
ty_let [constructor, in Definitions]
ty_new_elim [constructor, in Definitions]
ty_new_intro [constructor, in Definitions]
ty_all_elim [constructor, in Definitions]
ty_all_intro [constructor, in Definitions]
ty_var [constructor, in Definitions]
ty_trm [inductive, in Definitions]
ty_new_intro_p [constructor, in PreciseTyping]
ty_all_intro_p [constructor, in PreciseTyping]
ty_val_p [inductive, in PreciseTyping]
ty_top_inv_v [constructor, in InvertibleTyping]
ty_and_inv_v [constructor, in InvertibleTyping]
ty_sel_inv_v [constructor, in InvertibleTyping]
ty_all_inv_v [constructor, in InvertibleTyping]
ty_precise_inv_v [constructor, in InvertibleTyping]
ty_val_inv [inductive, in InvertibleTyping]
ty_top_inv [constructor, in InvertibleTyping]
ty_sel_inv [constructor, in InvertibleTyping]
ty_and_inv [constructor, in InvertibleTyping]
ty_all_inv [constructor, in InvertibleTyping]
ty_bnd_inv [constructor, in InvertibleTyping]
ty_dec_typ_inv [constructor, in InvertibleTyping]
ty_dec_trm_inv [constructor, in InvertibleTyping]
ty_precise_inv [constructor, in InvertibleTyping]
ty_var_inv [inductive, in InvertibleTyping]


U

unique_rcd_typ [lemma, in RecordAndInertTypes]


V

val [inductive, in Definitions]
val_mu_to_new [lemma, in CanonicalForms]
val_typ_all_to_lambda [lemma, in CanonicalForms]
val_mut [definition, in Definitions]
val_lambda [constructor, in Definitions]
val_new [constructor, in Definitions]
val_typing [lemma, in Safety]
var_typ_rcd_to_binds [lemma, in CanonicalForms]
var_typ_all_to_binds [lemma, in CanonicalForms]
var_typing_implies_avar_f [lemma, in Binding]


W

Weakening [library]
weaken_subtyp [lemma, in Weakening]
weaken_ty_trm [lemma, in Weakening]
weaken_rules [lemma, in Weakening]
well_typed_notin_dom [lemma, in CanonicalForms]
well_typed_to_ok_G [lemma, in CanonicalForms]
well_typed_push [constructor, in Definitions]
well_typed_empty [constructor, in Definitions]
well_typed [inductive, in Definitions]


X

x_bound_unique [lemma, in PreciseTyping]


other

_ ⊢# _ <: _ [notation, in TightTyping]
_ ⊢# _ : _ [notation, in TightTyping]
_ ⪯ _ [notation, in Subenvironments]
_ ⊢ _ <: _ [notation, in Definitions]
_ /- _ :: _ [notation, in Definitions]
_ /- _ : _ [notation, in Definitions]
_ ⊢ _ : _ [notation, in Definitions]
_ ⊢! _ : _ ⪼ _ [notation, in PreciseTyping]
_ ⊢!v _ : _ [notation, in PreciseTyping]
_ |-> _ [notation, in OperationalSemantics]
_ ⊢##v _ : _ [notation, in InvertibleTyping]
_ ⊢## _ : _ [notation, in InvertibleTyping]
⊢ _ : _ [notation, in Safety]



Notation Index

other

_ ⊢# _ <: _ [in TightTyping]
_ ⊢# _ : _ [in TightTyping]
_ ⪯ _ [in Subenvironments]
_ ⊢ _ <: _ [in Definitions]
_ /- _ :: _ [in Definitions]
_ /- _ : _ [in Definitions]
_ ⊢ _ : _ [in Definitions]
_ ⊢! _ : _ ⪼ _ [in PreciseTyping]
_ ⊢!v _ : _ [in PreciseTyping]
_ |-> _ [in OperationalSemantics]
_ ⊢##v _ : _ [in InvertibleTyping]
_ ⊢## _ : _ [in InvertibleTyping]
⊢ _ : _ [in Safety]



Library Index

B

Binding


C

CanonicalForms


D

Definitions


G

GeneralToTight


I

InvertibleTyping


N

Narrowing


O

OperationalSemantics


P

PreciseTyping


R

RecordAndInertTypes


S

Safety
Subenvironments
Substitution


T

TightTyping


W

Weakening



Lemma Index

B

binds_inert [in PreciseTyping]


C

canonical_forms_obj [in CanonicalForms]
canonical_forms_fun [in CanonicalForms]
corresponding_types [in CanonicalForms]


D

defs_has_hasnt_neq [in CanonicalForms]
defs_has_inv [in RecordAndInertTypes]


F

fv_ctx_types_push_eq [in Binding]


G

general_to_tight_typing [in GeneralToTight]
general_to_tight [in GeneralToTight]


H

hasnt_notin [in RecordAndInertTypes]


I

inert_concat [in RecordAndInertTypes]
inert_ok [in PreciseTyping]
inert_precise_all_inv [in PreciseTyping]
invertible_val_to_precise_lambda [in CanonicalForms]
invertible_typing_closure_tight_v [in InvertibleTyping]
invertible_typing_closure_tight [in InvertibleTyping]
invertible_to_precise_typ_all [in InvertibleTyping]
invertible_to_precise_trm_dec [in InvertibleTyping]
invert_fv_ctx_types_push [in Binding]


N

narrow_subtyping [in Narrowing]
narrow_typing [in Narrowing]
narrow_rules [in Narrowing]


O

opening_preserves_labels [in RecordAndInertTypes]
open_fresh_typ_dec_injective [in Binding]
open_fresh_avar_injective [in Binding]
open_record_type [in RecordAndInertTypes]
open_record_typ [in RecordAndInertTypes]
open_record_dec [in RecordAndInertTypes]
open_dec_preserves_label [in RecordAndInertTypes]


P

pf_dec_typ_inv [in PreciseTyping]
pf_inert_unique_tight_bounds [in PreciseTyping]
pf_record_unique_tight_bounds_rec [in PreciseTyping]
pf_record_sub [in PreciseTyping]
pf_psel_false [in PreciseTyping]
pf_bot_false [in PreciseTyping]
pf_inert_lambda_U [in PreciseTyping]
pf_inert_rcd_typ_U [in PreciseTyping]
pf_inert_rcd_U [in PreciseTyping]
pf_inert_bnd_U [in PreciseTyping]
pf_bnd_same_or_rcd [in PreciseTyping]
pf_rcd_T [in PreciseTyping]
pf_inert_T [in PreciseTyping]
pf_binds [in PreciseTyping]
precise_to_general_v [in PreciseTyping]
precise_to_general [in PreciseTyping]
precise_flow_record_has [in PreciseTyping]
precise_inert_typ [in PreciseTyping]
precise_flow_all_inv [in PreciseTyping]
preservation [in Safety]
preservation_helper [in Safety]
progress [in Safety]


R

record_has_ty_defs [in CanonicalForms]
record_typ_has_label_in [in RecordAndInertTypes]
record_type_open [in RecordAndInertTypes]
renaming_fresh [in Substitution]
renaming_typ [in Substitution]
renaming_def [in Substitution]


S

sel_replacement [in GeneralToTight]
sel_premise [in GeneralToTight]
subenv_implies_ok [in Subenvironments]
subenv_last [in Subenvironments]
subenv_push [in Subenvironments]
subenv_refl [in Subenvironments]
subst_ty_defs [in Substitution]
subst_ty_trm [in Substitution]
subst_rules [in Substitution]
subst_defs_hasnt [in Binding]
subst_label_of_def [in Binding]
subst_intro_typ [in Binding]
subst_intro_defs [in Binding]
subst_intro_trm [in Binding]
subst_open_commut_defs [in Binding]
subst_open_commut_trm [in Binding]
subst_open_commut_trm_val_def_defs [in Binding]
subst_open_commut_typ [in Binding]
subst_open_commut_typ_dec [in Binding]
subst_open_commut_avar [in Binding]
subst_fresh_ctx [in Binding]
subst_fresh_trm_val_def_defs [in Binding]
subst_fresh_typ_dec [in Binding]
subst_fresh_avar [in Binding]


T

tight_to_general [in TightTyping]
tight_to_invertible_v [in InvertibleTyping]
tight_to_invertible [in InvertibleTyping]
typing_implies_bound [in CanonicalForms]
ty_defs_record_type [in RecordAndInertTypes]


U

unique_rcd_typ [in RecordAndInertTypes]


V

val_mu_to_new [in CanonicalForms]
val_typ_all_to_lambda [in CanonicalForms]
val_typing [in Safety]
var_typ_rcd_to_binds [in CanonicalForms]
var_typ_all_to_binds [in CanonicalForms]
var_typing_implies_avar_f [in Binding]


W

weaken_subtyp [in Weakening]
weaken_ty_trm [in Weakening]
weaken_rules [in Weakening]
well_typed_notin_dom [in CanonicalForms]
well_typed_to_ok_G [in CanonicalForms]


X

x_bound_unique [in PreciseTyping]



Constructor Index

A

avar_f [in Definitions]
avar_b [in Definitions]


D

dec_trm [in Definitions]
dec_typ [in Definitions]
defs_cons [in Definitions]
defs_nil [in Definitions]
def_trm [in Definitions]
def_typ [in Definitions]


I

inert_all [in RecordAndInertTypes]
inert_empty [in RecordAndInertTypes]
inert_typ_bnd [in RecordAndInertTypes]
inert_typ_all [in RecordAndInertTypes]


L

label_trm [in Definitions]
label_typ [in Definitions]


N

nf_val [in OperationalSemantics]
nf_var [in OperationalSemantics]


P

pf_and2 [in PreciseTyping]
pf_and1 [in PreciseTyping]
pf_open [in PreciseTyping]
pf_bind [in PreciseTyping]


R

rd_trm [in RecordAndInertTypes]
rd_typ [in RecordAndInertTypes]
red_let_tgt [in OperationalSemantics]
red_let_var [in OperationalSemantics]
red_let_val [in OperationalSemantics]
red_app [in OperationalSemantics]
red_sel [in OperationalSemantics]
rh_andr [in RecordAndInertTypes]
rh_andl [in RecordAndInertTypes]
rh_one [in RecordAndInertTypes]
rt_cons [in RecordAndInertTypes]
rt_one [in RecordAndInertTypes]


S

sta_trm_typ_c [in Safety]
subenv_grow [in Subenvironments]
subenv_empty [in Subenvironments]
subtyp_all_t [in TightTyping]
subtyp_sel1_t [in TightTyping]
subtyp_sel2_t [in TightTyping]
subtyp_typ_t [in TightTyping]
subtyp_fld_t [in TightTyping]
subtyp_and2_t [in TightTyping]
subtyp_and12_t [in TightTyping]
subtyp_and11_t [in TightTyping]
subtyp_trans_t [in TightTyping]
subtyp_refl_t [in TightTyping]
subtyp_bot_t [in TightTyping]
subtyp_top_t [in TightTyping]
subtyp_all [in Definitions]
subtyp_sel1 [in Definitions]
subtyp_sel2 [in Definitions]
subtyp_typ [in Definitions]
subtyp_fld [in Definitions]
subtyp_and2 [in Definitions]
subtyp_and12 [in Definitions]
subtyp_and11 [in Definitions]
subtyp_trans [in Definitions]
subtyp_refl [in Definitions]
subtyp_bot [in Definitions]
subtyp_top [in Definitions]


T

trm_let [in Definitions]
trm_app [in Definitions]
trm_sel [in Definitions]
trm_val [in Definitions]
trm_var [in Definitions]
typ_all [in Definitions]
typ_bnd [in Definitions]
typ_sel [in Definitions]
typ_and [in Definitions]
typ_rcd [in Definitions]
typ_bot [in Definitions]
typ_top [in Definitions]
ty_sub_t [in TightTyping]
ty_and_intro_t [in TightTyping]
ty_rec_elim_t [in TightTyping]
ty_rec_intro_t [in TightTyping]
ty_let_t [in TightTyping]
ty_new_elim_t [in TightTyping]
ty_new_intro_t [in TightTyping]
ty_all_elim_t [in TightTyping]
ty_all_intro_t [in TightTyping]
ty_var_t [in TightTyping]
ty_defs_cons [in Definitions]
ty_defs_one [in Definitions]
ty_def_trm [in Definitions]
ty_def_typ [in Definitions]
ty_sub [in Definitions]
ty_and_intro [in Definitions]
ty_rec_elim [in Definitions]
ty_rec_intro [in Definitions]
ty_let [in Definitions]
ty_new_elim [in Definitions]
ty_new_intro [in Definitions]
ty_all_elim [in Definitions]
ty_all_intro [in Definitions]
ty_var [in Definitions]
ty_new_intro_p [in PreciseTyping]
ty_all_intro_p [in PreciseTyping]
ty_top_inv_v [in InvertibleTyping]
ty_and_inv_v [in InvertibleTyping]
ty_sel_inv_v [in InvertibleTyping]
ty_all_inv_v [in InvertibleTyping]
ty_precise_inv_v [in InvertibleTyping]
ty_top_inv [in InvertibleTyping]
ty_sel_inv [in InvertibleTyping]
ty_and_inv [in InvertibleTyping]
ty_all_inv [in InvertibleTyping]
ty_bnd_inv [in InvertibleTyping]
ty_dec_typ_inv [in InvertibleTyping]
ty_dec_trm_inv [in InvertibleTyping]
ty_precise_inv [in InvertibleTyping]


V

val_lambda [in Definitions]
val_new [in Definitions]


W

well_typed_push [in Definitions]
well_typed_empty [in Definitions]



Axiom Index

T

trm_label [in Definitions]
typ_label [in Definitions]



Inductive Index

A

avar [in Definitions]


D

dec [in Definitions]
def [in Definitions]
defs [in Definitions]


I

inert [in RecordAndInertTypes]
inert_typ [in RecordAndInertTypes]


L

label [in Definitions]


N

norm_form [in OperationalSemantics]


P

precise_flow [in PreciseTyping]


R

record_has [in RecordAndInertTypes]
record_typ [in RecordAndInertTypes]
record_dec [in RecordAndInertTypes]
red [in OperationalSemantics]


S

sta_trm_typ [in Safety]
subenv [in Subenvironments]
subtyp [in Definitions]
subtyp_t [in TightTyping]


T

trm [in Definitions]
typ [in Definitions]
ty_trm_t [in TightTyping]
ty_defs [in Definitions]
ty_def [in Definitions]
ty_trm [in Definitions]
ty_val_p [in PreciseTyping]
ty_val_inv [in InvertibleTyping]
ty_var_inv [in InvertibleTyping]


V

val [in Definitions]


W

well_typed [in Definitions]



Definition Index

C

ctx [in Definitions]


D

dec_mut [in Definitions]
defs_mut [in Definitions]
defs_hasnt [in Definitions]
defs_has [in Definitions]
def_mut [in Definitions]


F

fv_sta_vals [in Definitions]
fv_ctx_types [in Definitions]
fv_defs [in Definitions]
fv_def [in Definitions]
fv_val [in Definitions]
fv_trm [in Definitions]
fv_dec [in Definitions]
fv_typ [in Definitions]
fv_avar [in Definitions]


G

get_def [in Definitions]


L

label_of_dec [in Definitions]
label_of_def [in Definitions]


O

open_defs [in Definitions]
open_def [in Definitions]
open_val [in Definitions]
open_trm [in Definitions]
open_dec [in Definitions]
open_typ [in Definitions]
open_avar [in Definitions]
open_rec_defs [in Definitions]
open_rec_def [in Definitions]
open_rec_val [in Definitions]
open_rec_trm [in Definitions]
open_rec_dec [in Definitions]
open_rec_typ [in Definitions]
open_rec_avar [in Definitions]


R

record_type [in RecordAndInertTypes]
rules_mutind [in Definitions]
rules_subtyp [in Definitions]
rules_defs_mut [in Definitions]
rules_def_mut [in Definitions]
rules_trm_mut [in Definitions]


S

sta [in Definitions]
subst_fvar [in Binding]
subst_fresh_typ [in Binding]
subst_env [in Binding]
subst_ctx [in Binding]
subst_defs [in Binding]
subst_def [in Binding]
subst_val [in Binding]
subst_trm [in Binding]
subst_dec [in Binding]
subst_typ [in Binding]
subst_avar [in Binding]


T

trm_mutind [in Definitions]
trm_mut [in Definitions]
ts_t_mutind [in TightTyping]
ts_subtyp_t [in TightTyping]
ts_ty_trm_t_mut [in TightTyping]
ts_mutind [in Definitions]
ts_subtyp [in Definitions]
ts_ty_trm_mut [in Definitions]
typ_mutind [in Definitions]
typ_mut [in Definitions]


V

val_mut [in Definitions]



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 (331 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 (13 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 (14 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 (99 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 (114 entries)
Axiom Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ other (2 entries)
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 (28 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 (61 entries)