| 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 | (335 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 | (105 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 | (112 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 | (27 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 | (62 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_typing_closure_tight_v [lemma, in InvertibleTyping]
invertible_typing_closure_tight [lemma, in InvertibleTyping]
invertible_val_to_precise_lambda [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_ok_r [lemma, in Subenvironments]
subenv_ok_l [lemma, in Subenvironments]
subenv_ok_fresh [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_ctx_push [lemma, 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_push [lemma, in CanonicalForms]
well_typed_empty [lemma, in CanonicalForms]
well_typed_notin_dom [lemma, in CanonicalForms]
well_typed_to_ok_s [lemma, in CanonicalForms]
well_typed_to_ok_G [lemma, in CanonicalForms]
well_typed [definition, 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
BindingC
CanonicalFormsD
DefinitionsG
GeneralToTightI
InvertibleTypingN
NarrowingO
OperationalSemanticsP
PreciseTypingR
RecordAndInertTypesS
SafetySubenvironments
Substitution
T
TightTypingW
WeakeningLemma 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_typing_closure_tight_v [in InvertibleTyping]
invertible_typing_closure_tight [in InvertibleTyping]
invertible_val_to_precise_lambda [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_ok_r [in Subenvironments]
subenv_ok_l [in Subenvironments]
subenv_ok_fresh [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_ctx_push [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_push [in CanonicalForms]
well_typed_empty [in CanonicalForms]
well_typed_notin_dom [in CanonicalForms]
well_typed_to_ok_s [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]
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]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]W
well_typed [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 | (335 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 | (105 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 | (112 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 | (27 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 | (62 entries) |