A Proof of Virtual Types
| 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 |
_ |
(769 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 |
_ |
(27 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 |
_ |
(303 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 |
_ |
(94 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 |
_ |
(40 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 |
_ |
(235 entries) |
| Module Index |
A |
B |
C |
D |
E |
F |
G |
H |
I |
J |
K |
L |
M |
N |
O |
P |
Q |
R |
S |
T |
U |
V |
W |
X |
Y |
Z |
_ |
(48 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 |
_ |
(22 entries) |
Global Index
A
A [definition, in Proofs_TypeOrdering]
A [definition, in Proofs_TypeOrdering]
amplitude [definition, in DeBruijn]
amplitude [definition, in DeBruijn]
amplitude [definition, in DeBruijn]
amplitude [definition, in DeBruijn]
applyTo [definition, in Typing]
applyTo [definition, in Typing]
applyTo [axiom, in Typing]
args_are_correct [definition, in Proofs_SubstitutionLemmas2]
args_conform_to_params [definition, in Proofs_SubstitutionLemmas2]
C
Calculus [library]
classEnv [definition, in Typing]
classes_are_well_formed [definition, in WellFormedness]
classes_are_well_formed_proof [lemma, in Proofs_Miscellaneous]
classes_smaller_than_types [definition, in WellFormedness]
classes_smaller_than_types_proof [lemma, in Proofs_Miscellaneous]
classSuper [axiom, in Calculus]
ClassSym [axiom, in Calculus]
ClassSym_eq [axiom, in Calculus]
cons_destruct [lemma, in Util]
context_is_well_formed [inductive, in Proofs_SubstitutionLemmas]
context_is_well_formed_intro [constructor, in Proofs_SubstitutionLemmas]
D
DeBruijn [library]
drop_at_depth_in_fieldTermList [definition, in DeBruijn]
drop_at_depth_in_paramTermList [definition, in DeBruijn]
drop_at_depth_in_path [definition, in DeBruijn]
drop_at_depth_in_term [definition, in DeBruijn]
drop_at_depth_in_type [definition, in DeBruijn]
drop_in_path [definition, in DeBruijn]
drop_in_term [definition, in DeBruijn]
drop_in_type [definition, in DeBruijn]
E
empty_is_empty_1 [lemma, in Util]
empty_is_empty_2 [lemma, in Util]
empty_paramset [definition, in Typing]
empty_union_left [lemma, in Util]
empty_union_right [lemma, in Util]
empty_varset [definition, in DeBruijn]
Env [inductive, in Typing]
Env_mk [constructor, in Typing]
eqA [definition, in Proofs_TypeOrdering]
eqA [definition, in Proofs_TypeOrdering]
eqA_dec [definition, in Proofs_TypeOrdering]
eqA_dec [definition, in Proofs_TypeOrdering]
ESM [module, in Proofs_TypeOrdering]
ESM [module, in Proofs_TypeOrdering]
Evaluate [inductive, in Semantics]
EvaluateMain [definition, in Semantics]
Evaluate_end [constructor, in Semantics]
Evaluate_step [constructor, in Semantics]
F
fieldDefs_are_well_formed [definition, in WellFormedness]
fieldOwner [axiom, in Calculus]
FieldSym [axiom, in Calculus]
FieldSym_eq [axiom, in Calculus]
fields_evaluated [definition, in Proofs_Progress]
fields_of_fieldTermList [definition, in Typing]
fields_of_fieldValueList [definition, in Typing]
FieldTermList [inductive, in Calculus]
FieldTermListTyping [inductive, in Typing]
FieldTermListTyping_cons [constructor, in Typing]
FieldTermListTyping_nil [constructor, in Typing]
FieldTerm_cons [constructor, in Calculus]
FieldTerm_nil [constructor, in Calculus]
fieldType [axiom, in Calculus]
fieldTypes_are_well_formed [lemma, in Proofs_Miscellaneous]
FieldValueList [inductive, in Calculus]
FieldValueListTyping [inductive, in Typing]
FieldValueListTyping_cons [constructor, in Typing]
FieldValueListTyping_nil [constructor, in Typing]
FieldValueList_contains [inductive, in Subclassing]
FieldValueList_contains_head [constructor, in Subclassing]
FieldValueList_contains_tail [constructor, in Subclassing]
FieldValueList_eqdec' [definition, in Proofs_Miscellaneous]
fieldValueList_to_fieldTermList [definition, in Subclassing]
FieldValue_cons [constructor, in Calculus]
FieldValue_nil [constructor, in Calculus]
forall_is_listForall [lemma, in Proofs_SubstitutionLemmas]
fp_and_paramSubst_in_path [lemma, in Proofs_Miscellaneous]
fp_and_paramSubst_in_type [lemma, in Proofs_Miscellaneous]
fp_in_fieldTermList [definition, in Typing]
fp_in_paramTermList [definition, in Typing]
fp_in_path [definition, in Typing]
fp_in_term [definition, in Typing]
fp_in_type [definition, in Typing]
free_parameters_and_lifting_aux_0 [lemma, in Proofs_Miscellaneous]
free_parameters_and_lifting_aux_2 [lemma, in Proofs_Miscellaneous]
free_parameters_and_lifting_0 [lemma, in Proofs_Miscellaneous]
free_parameters_and_lifting_2 [lemma, in Proofs_Miscellaneous]
fun_extension [definition, in WellFoundation]
fv_and_paramSubst_in_path [lemma, in Proofs_Miscellaneous]
fv_and_paramSubst_in_type [lemma, in Proofs_Miscellaneous]
fv_and_thisSubst_in_path [lemma, in DeBruijn]
fv_and_thisSubst_in_type [lemma, in DeBruijn]
fv_and_var_in_path [lemma, in DeBruijn]
fv_and_var_in_path1 [lemma, in DeBruijn]
fv_and_var_in_path2 [lemma, in DeBruijn]
fv_and_var_in_type [lemma, in DeBruijn]
fv_and_var_in_type1 [lemma, in DeBruijn]
fv_and_var_in_type2 [lemma, in DeBruijn]
fv_at_depth_in_fieldTermList [definition, in DeBruijn]
fv_at_depth_in_paramTermList [definition, in DeBruijn]
fv_at_depth_in_path [definition, in DeBruijn]
fv_at_depth_in_term [definition, in DeBruijn]
fv_at_depth_in_type [definition, in DeBruijn]
fv_in_fieldTermList [definition, in DeBruijn]
fv_in_paramTermList [definition, in DeBruijn]
fv_in_path [definition, in DeBruijn]
fv_in_term [definition, in DeBruijn]
fv_in_type [definition, in DeBruijn]
fv_pathvar_empty [lemma, in DeBruijn]
fv_pathvar_non_empty [lemma, in DeBruijn]
fv_termvar_empty [lemma, in DeBruijn]
fv_termvar_non_empty [lemma, in DeBruijn]
G
Gen_FieldValueListTyping [inductive, in Typing]
Gen_FieldValueListTyping_cons [constructor, in Typing]
Gen_FieldValueListTyping_nil [constructor, in Typing]
Gen_PathTyping [inductive, in Typing]
Gen_P_Param [constructor, in Typing]
Gen_P_This [constructor, in Typing]
Gen_P_Value [constructor, in Typing]
Gen_P_Var [constructor, in Typing]
Gen_Subtyping [inductive, in Typing]
Gen_S_Alias_Left [constructor, in Typing]
Gen_S_Alias_Right [constructor, in Typing]
Gen_S_Class [constructor, in Typing]
Gen_S_Down [constructor, in Typing]
Gen_S_Extends [constructor, in Typing]
Gen_S_Trans [constructor, in Typing]
Gen_S_Up [constructor, in Typing]
Gen_S_Virtual [constructor, in Typing]
I
IsComplete [inductive, in Typing]
IsComplete_fields [definition, in Typing]
IsComplete_intro [constructor, in Typing]
IsComplete_methods [definition, in Typing]
IsComplete_params [definition, in Typing]
IsComplete_types [definition, in Typing]
K
Kinding [inductive, in WellFormedness]
K_Class [constructor, in WellFormedness]
K_Virtual [constructor, in WellFormedness]
L
lemmaA1 [lemma, in Proofs_Miscellaneous]
lemmaA10_0 [lemma, in Proofs_Miscellaneous]
lemmaA10_2 [lemma, in Proofs_Miscellaneous]
lemmaA12 [lemma, in Proofs_TypeOrdering]
lemmaA12' [lemma, in Proofs_TypeOrdering]
lemmaA13_1 [lemma, in Proofs_TypeOrdering]
lemmaA13_1' [lemma, in Proofs_TypeOrdering]
lemmaA13_2 [lemma, in Proofs_TypeOrdering]
lemmaA13_3 [lemma, in Proofs_TypeOrdering]
lemmaA14 [lemma, in Proofs_TypeOrdering]
lemmaA15_1 [lemma, in Proofs_TypeOrdering]
lemmaA15_2 [lemma, in Proofs_TypeOrdering]
lemmaA17 [lemma, in Proofs_TypeOrdering]
lemmaA18 [lemma, in Proofs_TypeOrdering]
lemmaA18_aux_1 [lemma, in Proofs_TypeOrdering]
lemmaA18_aux_2 [lemma, in Proofs_TypeOrdering]
lemmaA19 [lemma, in Proofs_Subclassing]
lemmaA1_for_paths [lemma, in Proofs_SubstitutionLemmas]
lemmaA20 [lemma, in Proofs_Subclassing]
lemmaA21 [lemma, in Proofs_Subclassing]
lemmaA21_aux [lemma, in Proofs_Subclassing]
lemmaA22 [lemma, in Proofs_Subclassing]
lemmaA23_prop1 [definition, in Proofs_AdmissibilityOfTransitivity]
lemmaA23_prop2 [definition, in Proofs_AdmissibilityOfTransitivity]
lemmaA23_prop3 [definition, in Proofs_AdmissibilityOfTransitivity]
lemmaA23_1 [lemma, in Proofs_AdmissibilityOfTransitivity]
lemmaA23_2 [lemma, in Proofs_AdmissibilityOfTransitivity]
lemmaA24_aux [lemma, in Proofs_Miscellaneous]
lemmaA24_prop_1 [definition, in Proofs_AdmissibilityOfTransitivity]
lemmaA24_prop_2 [definition, in Proofs_AdmissibilityOfTransitivity]
lemmaA24_prop_3 [definition, in Proofs_AdmissibilityOfTransitivity]
lemmaA24_2 [lemma, in Proofs_AdmissibilityOfTransitivity]
lemmaA24_2_aux [lemma, in Proofs_AdmissibilityOfTransitivity]
lemmaA25 [lemma, in Proofs_AdmissibilityOfTransitivity]
lemmaA26_prop_1 [definition, in Proofs_AdmissibilityOfTransitivity]
lemmaA26_prop_2 [definition, in Proofs_AdmissibilityOfTransitivity]
lemmaA26_1 [lemma, in Proofs_AdmissibilityOfTransitivity]
lemmaA26_1_aux [lemma, in Proofs_AdmissibilityOfTransitivity]
lemmaA26_2 [lemma, in Proofs_AdmissibilityOfTransitivity]
lemmaA26_2_aux [lemma, in Proofs_AdmissibilityOfTransitivity]
lemmaA27 [lemma, in Proofs_AdmissibilityOfTransitivity]
lemmaA27_prop [definition, in Proofs_AdmissibilityOfTransitivity]
lemmaA28_prop1 [definition, in Proofs_AdmissibilityOfTransitivity]
lemmaA28_prop2 [definition, in Proofs_AdmissibilityOfTransitivity]
lemmaA28_prop3 [definition, in Proofs_AdmissibilityOfTransitivity]
lemmaA28_1 [lemma, in Proofs_AdmissibilityOfTransitivity]
lemmaA28_2 [lemma, in Proofs_AdmissibilityOfTransitivity]
lemmaA29 [lemma, in Proofs_Progress]
lemmaA29_aux_1 [lemma, in Proofs_Progress]
lemmaA29_aux_2 [lemma, in Proofs_Progress]
lemmaA29_aux_2_prop1 [definition, in Proofs_Progress]
lemmaA29_aux_2_prop2 [definition, in Proofs_Progress]
lemmaA29_aux_2_prop3 [definition, in Proofs_Progress]
lemmaA29_aux_3 [lemma, in Proofs_Progress]
lemmaA29_prop1 [definition, in Proofs_Progress]
lemmaA29_prop2 [definition, in Proofs_Progress]
lemmaA29_prop3 [definition, in Proofs_Progress]
lemmaA2_1 [lemma, in Proofs_Miscellaneous]
lemmaA2_2 [lemma, in Proofs_Miscellaneous]
lemmaA30_0 [lemma, in Proofs_DeBruijnSIndices]
lemmaA30_0' [lemma, in Proofs_DeBruijnSIndices]
lemmaA30_1 [lemma, in Proofs_DeBruijnSIndices]
lemmaA30_1' [lemma, in Proofs_DeBruijnSIndices]
lemmaA30_1_prop1 [definition, in Proofs_DeBruijnSIndices]
lemmaA30_1_prop2 [definition, in Proofs_DeBruijnSIndices]
lemmaA30_1_prop3 [definition, in Proofs_DeBruijnSIndices]
lemmaA30_2 [lemma, in Proofs_DeBruijnSIndices]
lemmaA30_2' [lemma, in Proofs_DeBruijnSIndices]
lemmaA31_0 [lemma, in Proofs_DeBruijnSIndices]
lemmaA31_0' [lemma, in Proofs_DeBruijnSIndices]
lemmaA31_1 [lemma, in Proofs_DeBruijnSIndices]
lemmaA31_1' [lemma, in Proofs_DeBruijnSIndices]
lemmaA31_1_prop1 [definition, in Proofs_DeBruijnSIndices]
lemmaA31_1_prop2 [definition, in Proofs_DeBruijnSIndices]
lemmaA31_1_prop3 [definition, in Proofs_DeBruijnSIndices]
lemmaA31_2 [lemma, in Proofs_DeBruijnSIndices]
lemmaA31_2' [lemma, in Proofs_DeBruijnSIndices]
lemmaA32 [lemma, in Proofs_DeBruijnSIndices]
lemmaA32_prop1 [definition, in Proofs_DeBruijnSIndices]
lemmaA32_prop2 [definition, in Proofs_DeBruijnSIndices]
lemmaA33_0 [lemma, in Proofs_DeBruijnSIndices]
lemmaA33_0' [lemma, in Proofs_DeBruijnSIndices]
lemmaA33_1 [lemma, in Proofs_DeBruijnSIndices]
lemmaA33_1' [lemma, in Proofs_DeBruijnSIndices]
lemmaA33_1_prop1 [definition, in Proofs_DeBruijnSIndices]
lemmaA33_1_prop2 [definition, in Proofs_DeBruijnSIndices]
lemmaA33_1_prop3 [definition, in Proofs_DeBruijnSIndices]
lemmaA33_2 [lemma, in Proofs_DeBruijnSIndices]
lemmaA33_2' [lemma, in Proofs_DeBruijnSIndices]
lemmaA34_0 [lemma, in Proofs_DeBruijnSIndices]
lemmaA34_0' [lemma, in Proofs_DeBruijnSIndices]
lemmaA34_1 [lemma, in Proofs_DeBruijnSIndices]
lemmaA34_1' [lemma, in Proofs_DeBruijnSIndices]
lemmaA34_1_prop1 [definition, in Proofs_DeBruijnSIndices]
lemmaA34_1_prop2 [definition, in Proofs_DeBruijnSIndices]
lemmaA34_1_prop3 [definition, in Proofs_DeBruijnSIndices]
lemmaA34_2 [lemma, in Proofs_DeBruijnSIndices]
lemmaA34_2' [lemma, in Proofs_DeBruijnSIndices]
lemmaA35_0 [lemma, in Proofs_DeBruijnSIndices]
lemmaA35_0' [lemma, in Proofs_DeBruijnSIndices]
lemmaA35_1 [lemma, in Proofs_DeBruijnSIndices]
lemmaA35_1' [lemma, in Proofs_DeBruijnSIndices]
lemmaA35_1_prop1 [definition, in Proofs_DeBruijnSIndices]
lemmaA35_1_prop2 [definition, in Proofs_DeBruijnSIndices]
lemmaA35_1_prop3 [definition, in Proofs_DeBruijnSIndices]
lemmaA35_2 [lemma, in Proofs_DeBruijnSIndices]
lemmaA35_2' [lemma, in Proofs_DeBruijnSIndices]
lemmaA36_32 [lemma, in Proofs_DeBruijnSIndices]
lemmaA36_32_prop1 [definition, in Proofs_DeBruijnSIndices]
lemmaA36_32_prop2 [definition, in Proofs_DeBruijnSIndices]
lemmaA36_33_0 [lemma, in Proofs_DeBruijnSIndices]
lemmaA36_33_0' [lemma, in Proofs_DeBruijnSIndices]
lemmaA36_33_1 [lemma, in Proofs_DeBruijnSIndices]
lemmaA36_33_1' [lemma, in Proofs_DeBruijnSIndices]
lemmaA36_33_1_prop1 [definition, in Proofs_DeBruijnSIndices]
lemmaA36_33_1_prop2 [definition, in Proofs_DeBruijnSIndices]
lemmaA36_33_1_prop3 [definition, in Proofs_DeBruijnSIndices]
lemmaA36_33_2 [lemma, in Proofs_DeBruijnSIndices]
lemmaA36_33_2' [lemma, in Proofs_DeBruijnSIndices]
lemmaA36_34_0 [lemma, in Proofs_DeBruijnSIndices]
lemmaA36_34_0' [lemma, in Proofs_DeBruijnSIndices]
lemmaA36_34_1 [lemma, in Proofs_DeBruijnSIndices]
lemmaA36_34_1' [lemma, in Proofs_DeBruijnSIndices]
lemmaA36_34_1_prop1 [definition, in Proofs_DeBruijnSIndices]
lemmaA36_34_1_prop2 [definition, in Proofs_DeBruijnSIndices]
lemmaA36_34_1_prop3 [definition, in Proofs_DeBruijnSIndices]
lemmaA36_34_2 [lemma, in Proofs_DeBruijnSIndices]
lemmaA36_34_2' [lemma, in Proofs_DeBruijnSIndices]
lemmaA36_35_0 [lemma, in Proofs_DeBruijnSIndices]
lemmaA36_35_0' [lemma, in Proofs_DeBruijnSIndices]
lemmaA36_35_1 [lemma, in Proofs_DeBruijnSIndices]
lemmaA36_35_1' [lemma, in Proofs_DeBruijnSIndices]
lemmaA36_35_1_prop1 [definition, in Proofs_DeBruijnSIndices]
lemmaA36_35_1_prop2 [definition, in Proofs_DeBruijnSIndices]
lemmaA36_35_1_prop3 [definition, in Proofs_DeBruijnSIndices]
lemmaA36_35_2 [lemma, in Proofs_DeBruijnSIndices]
lemmaA36_35_2' [lemma, in Proofs_DeBruijnSIndices]
lemmaA37_0 [lemma, in Proofs_DeBruijnSIndices]
lemmaA37_0' [lemma, in Proofs_DeBruijnSIndices]
lemmaA37_1 [lemma, in Proofs_DeBruijnSIndices]
lemmaA37_1' [lemma, in Proofs_DeBruijnSIndices]
lemmaA37_1_prop1 [definition, in Proofs_DeBruijnSIndices]
lemmaA37_1_prop2 [definition, in Proofs_DeBruijnSIndices]
lemmaA37_1_prop3 [definition, in Proofs_DeBruijnSIndices]
lemmaA37_2 [lemma, in Proofs_DeBruijnSIndices]
lemmaA37_2' [lemma, in Proofs_DeBruijnSIndices]
lemmaA38_0 [lemma, in Proofs_SubstitutionLemmas]
lemmaA38_0_corollary [lemma, in Proofs_SubstitutionLemmas]
lemmaA38_0_prop1 [definition, in Proofs_SubstitutionLemmas]
lemmaA38_0_prop2 [definition, in Proofs_SubstitutionLemmas]
lemmaA38_0_prop3 [definition, in Proofs_SubstitutionLemmas]
lemmaA38_2 [lemma, in Proofs_SubstitutionLemmas]
lemmaA39_param1_prop1 [definition, in Proofs_SubstitutionLemmas2]
lemmaA39_param1_prop2 [definition, in Proofs_SubstitutionLemmas2]
lemmaA39_param1_prop3 [definition, in Proofs_SubstitutionLemmas2]
lemmaA39_param_aux_1 [lemma, in Proofs_SubstitutionLemmas2]
lemmaA39_param_aux_2 [lemma, in Proofs_SubstitutionLemmas2]
lemmaA39_param_aux_3 [lemma, in Proofs_SubstitutionLemmas2]
lemmaA39_param_aux_4 [lemma, in Proofs_SubstitutionLemmas2]
lemmaA39_param_aux_4_corollary [lemma, in Proofs_SubstitutionLemmas2]
lemmaA39_param_main [lemma, in Proofs_SubstitutionLemmas2]
lemmaA39_param_prop1 [definition, in Proofs_SubstitutionLemmas2]
lemmaA39_param_prop2 [definition, in Proofs_SubstitutionLemmas2]
lemmaA39_param_prop3 [definition, in Proofs_SubstitutionLemmas2]
lemmaA39_param_0 [lemma, in Proofs_SubstitutionLemmas2]
lemmaA39_param_1 [lemma, in Proofs_SubstitutionLemmas2]
lemmaA39_param_2 [lemma, in Proofs_SubstitutionLemmas2]
lemmaA39_this1_aux_1 [lemma, in Proofs_SubstitutionLemmas]
lemmaA39_this1_aux_2 [lemma, in Proofs_SubstitutionLemmas]
lemmaA39_this1_prop1 [definition, in Proofs_SubstitutionLemmas]
lemmaA39_this1_prop2 [definition, in Proofs_SubstitutionLemmas]
lemmaA39_this1_prop3 [definition, in Proofs_SubstitutionLemmas]
lemmaA39_this_main [lemma, in Proofs_SubstitutionLemmas]
lemmaA39_this_prop1 [definition, in Proofs_SubstitutionLemmas]
lemmaA39_this_prop2 [definition, in Proofs_SubstitutionLemmas]
lemmaA39_this_prop3 [definition, in Proofs_SubstitutionLemmas]
lemmaA39_this_0 [lemma, in Proofs_SubstitutionLemmas]
lemmaA39_this_1 [lemma, in Proofs_SubstitutionLemmas]
lemmaA39_this_2 [lemma, in Proofs_SubstitutionLemmas]
lemmaA39_var1_prop1 [definition, in Proofs_SubstitutionLemmas3]
lemmaA39_var1_prop2 [definition, in Proofs_SubstitutionLemmas3]
lemmaA39_var1_prop3 [definition, in Proofs_SubstitutionLemmas3]
lemmaA39_var_aux_1 [lemma, in Proofs_SubstitutionLemmas3]
lemmaA39_var_aux_2 [lemma, in Proofs_SubstitutionLemmas3]
lemmaA39_var_aux_3 [lemma, in Proofs_SubstitutionLemmas3]
lemmaA39_var_aux_4 [lemma, in Proofs_SubstitutionLemmas3]
lemmaA39_var_aux_5 [lemma, in Proofs_SubstitutionLemmas3]
lemmaA39_var_aux_6 [lemma, in Proofs_SubstitutionLemmas3]
lemmaA39_var_aux_7 [lemma, in Proofs_SubstitutionLemmas3]
lemmaA39_var_aux_8 [lemma, in Proofs_SubstitutionLemmas3]
lemmaA39_var_main [lemma, in Proofs_SubstitutionLemmas3]
lemmaA39_var_prop1 [definition, in Proofs_SubstitutionLemmas3]
lemmaA39_var_prop2 [definition, in Proofs_SubstitutionLemmas3]
lemmaA39_var_prop3 [definition, in Proofs_SubstitutionLemmas3]
lemmaA39_var_0 [lemma, in Proofs_SubstitutionLemmas3]
lemmaA39_var_1 [lemma, in Proofs_SubstitutionLemmas3]
lemmaA39_var_1_corollary [lemma, in Proofs_SubstitutionLemmas3]
lemmaA39_var_2 [lemma, in Proofs_SubstitutionLemmas3]
lemmaA3_aux_1 [lemma, in Proofs_Miscellaneous]
lemmaA3_prop1 [definition, in Proofs_Miscellaneous]
lemmaA3_prop2 [definition, in Proofs_Miscellaneous]
lemmaA3_0 [lemma, in Proofs_Miscellaneous]
lemmaA3_2 [lemma, in Proofs_Miscellaneous]
lemmaA3_3 [lemma, in Proofs_Miscellaneous]
lemmaA3_3_corollary [lemma, in Proofs_Miscellaneous]
lemmaA40 [lemma, in Proofs_SubjectReduction]
lemmaA40_aux_1 [lemma, in Proofs_SubjectReduction]
lemmaA40_aux_10 [lemma, in Proofs_SubstitutionLemmas]
lemmaA40_aux_11 [lemma, in Proofs_SubjectReduction]
lemmaA40_aux_12 [lemma, in Proofs_SubjectReduction]
lemmaA40_aux_13 [lemma, in Proofs_SubjectReduction]
lemmaA40_aux_14 [lemma, in Proofs_SubjectReduction]
lemmaA40_aux_15 [lemma, in Proofs_SubjectReduction]
lemmaA40_aux_16 [lemma, in Proofs_SubjectReduction]
lemmaA40_aux_2 [lemma, in Proofs_SubjectReduction]
lemmaA40_aux_3 [lemma, in Proofs_SubjectReduction]
lemmaA40_aux_4 [lemma, in Proofs_SubstitutionLemmas]
lemmaA40_aux_4_prop1 [definition, in Proofs_SubstitutionLemmas]
lemmaA40_aux_4_prop2 [definition, in Proofs_SubstitutionLemmas]
lemmaA40_aux_5 [lemma, in Proofs_SubjectReduction]
lemmaA40_aux_6 [lemma, in Proofs_SubjectReduction]
lemmaA40_aux_7 [lemma, in Proofs_SubjectReduction]
lemmaA40_aux_8 [lemma, in Proofs_SubstitutionLemmas]
lemmaA40_aux_8_prop1 [definition, in Proofs_SubstitutionLemmas]
lemmaA40_aux_8_prop2 [definition, in Proofs_SubstitutionLemmas]
lemmaA40_aux_9 [lemma, in Proofs_SubstitutionLemmas]
lemmaA40_prop1 [definition, in Proofs_SubjectReduction]
lemmaA40_prop2 [definition, in Proofs_SubjectReduction]
lemmaA40_prop3 [definition, in Proofs_SubjectReduction]
lemmaA41 [lemma, in Proofs_Soundness]
lemmaA42 [lemma, in Proofs_Soundness]
lemmaA4_prop1 [definition, in Proofs_Miscellaneous]
lemmaA4_prop2 [definition, in Proofs_Miscellaneous]
lemmaA4_0 [lemma, in Proofs_Miscellaneous]
lemmaA4_0' [lemma, in Proofs_Miscellaneous]
lemmaA4_0_corollary [lemma, in Proofs_Miscellaneous]
lemmaA4_1 [lemma, in Proofs_Miscellaneous]
lemmaA4_1_prop1 [definition, in Proofs_Miscellaneous]
lemmaA4_1_prop2 [definition, in Proofs_Miscellaneous]
lemmaA4_1_prop3 [definition, in Proofs_Miscellaneous]
lemmaA4_2 [lemma, in Proofs_Miscellaneous]
lemmaA4_2' [lemma, in Proofs_Miscellaneous]
lemmaA4_3 [lemma, in Proofs_Miscellaneous]
lemmaA4_3' [lemma, in Proofs_Miscellaneous]
lemmaA4_3_corollary [lemma, in Proofs_Miscellaneous]
lemmaA5 [lemma, in Proofs_Miscellaneous]
lemmaA5_P1 [definition, in Proofs_Miscellaneous]
lemmaA5_P2 [definition, in Proofs_Miscellaneous]
lemmaA6_1 [lemma, in Proofs_Miscellaneous]
lemmaA6_1' [lemma, in Proofs_Miscellaneous]
lemmaA6_2 [lemma, in Proofs_Miscellaneous]
lemmaA6_2' [lemma, in Proofs_Miscellaneous]
lemmaA6_3 [lemma, in Proofs_Miscellaneous]
lemmaA6_3' [lemma, in Proofs_Miscellaneous]
lemmaA7 [lemma, in Proofs_Miscellaneous]
lemmaA7' [lemma, in Proofs_Miscellaneous]
lemmaA8_1 [lemma, in Proofs_Miscellaneous]
lemmaA8_2 [lemma, in Proofs_Miscellaneous]
lemmaA9_aux_0 [lemma, in Proofs_Miscellaneous]
lemmaA9_0 [lemma, in Proofs_Miscellaneous]
lemmaA9_2 [lemma, in Proofs_Miscellaneous]
length_of_append [lemma, in Util]
length_of_map [lemma, in Util]
lift_at_depth_in_fieldTermList [definition, in DeBruijn]
lift_at_depth_in_paramTermList [definition, in DeBruijn]
lift_at_depth_in_path [definition, in DeBruijn]
lift_at_depth_in_term [definition, in DeBruijn]
lift_at_depth_in_type [definition, in DeBruijn]
lift_at_depth_in_var [definition, in DeBruijn]
lift_in_path [definition, in DeBruijn]
lift_in_term [definition, in DeBruijn]
lift_in_type [definition, in DeBruijn]
listForall_is_forall [lemma, in Proofs_SubstitutionLemmas]
List_disjoint [definition, in Typing]
list_forall [definition, in Proofs_SubstitutionLemmas]
List_sublist [definition, in Proofs_SubstitutionLemmas2]
local_types_well_formed [definition, in Proofs_SubstitutionLemmas]
local_types_well_formed_aux [definition, in Proofs_SubstitutionLemmas]
M
main [axiom, in Calculus]
main_term_is_well_typed [lemma, in Proofs_Miscellaneous]
map_elim [lemma, in Util]
map_intro [lemma, in Util]
map_of_append [lemma, in Util]
map_paramSubst_in_fieldTermList [definition, in Substitutions]
map_paramSubst_in_paramTermList [definition, in Substitutions]
map_paramSubst_in_path [definition, in Substitutions]
map_paramSubst_in_term [definition, in Substitutions]
map_paramSubst_in_type [definition, in Substitutions]
map_paramSubst_in_typeList [definition, in Proofs_SubstitutionLemmas2]
map_varSubst_in_typeList [definition, in Proofs_SubstitutionLemmas3]
MatchCompNat [library]
Match2 [lemma, in MatchCompNat]
Match2_diff [lemma, in MatchCompNat]
Match3 [lemma, in MatchCompNat]
Match3_diff [lemma, in MatchCompNat]
match_comp_nat2 [definition, in MatchCompNat]
match_comp_nat2_aux_0 [lemma, in MatchCompNat]
match_comp_nat2_aux_1 [lemma, in MatchCompNat]
match_comp_nat2_aux_2 [lemma, in MatchCompNat]
match_comp_nat2_ge [lemma, in MatchCompNat]
match_comp_nat2_lt [lemma, in MatchCompNat]
match_comp_nat3 [definition, in MatchCompNat]
match_comp_nat3_aux_1 [lemma, in MatchCompNat]
match_comp_nat3_aux_2 [lemma, in MatchCompNat]
match_comp_nat3_aux_3 [lemma, in MatchCompNat]
match_comp_nat3_eq [lemma, in MatchCompNat]
match_comp_nat3_gt [lemma, in MatchCompNat]
match_comp_nat3_lt [lemma, in MatchCompNat]
methodBody_of_type_methodType [lemma, in Proofs_Miscellaneous]
methodDefs_are_well_formed [definition, in WellFormedness]
methodOwner [axiom, in Calculus]
MethodSym [axiom, in Calculus]
MethodSym_eq [axiom, in Calculus]
methodType [axiom, in Calculus]
methodTypes_are_well_formed [lemma, in Proofs_Miscellaneous]
methodVals_are_well_formed [definition, in WellFormedness]
methodValue [axiom, in Calculus]
method_parameters [definition, in WellFormedness]
method_parameters_spec [axiom, in Calculus]
myarith_1 [lemma, in Util]
myarith_2 [lemma, in Util]
My_DeBruijn [module, in TypeOrdering]
My_Proofs_AdmissibilityOfTransitivity [module, in Proofs_Progress]
My_Proofs_DeBruijnSIndices [module, in Proofs_SubstitutionLemmas]
My_Proofs_Miscellaneous [module, in Proofs_TypeOrdering]
My_Proofs_Progress [module, in Proofs_DeBruijnSIndices]
My_Proofs_Subclassing [module, in Proofs_AdmissibilityOfTransitivity]
My_Proofs_SubjectReduction [module, in Proofs_Soundness]
My_Proofs_SubstitutionLemmas [module, in Proofs_SubstitutionLemmas2]
My_Proofs_SubstitutionLemmas2 [module, in Proofs_SubstitutionLemmas3]
My_Proofs_SubstitutionLemmas3 [module, in Proofs_SubjectReduction]
My_Proofs_TypeOrdering [module, in Proofs_Subclassing]
My_Semantics [module, in WellFormedness]
My_Subclassing [module, in Substitutions]
My_Substitutions [module, in DeBruijn]
My_TypeOrdering [module, in Typing]
My_Typing [module, in Semantics]
My_WellFormedness [module, in Proofs_Miscellaneous]
N
new_lemma1_0 [lemma, in Proofs_Miscellaneous]
new_lemma1_2 [lemma, in Proofs_Miscellaneous]
new_lemma2_0 [lemma, in Proofs_Miscellaneous]
new_lemma2_2 [lemma, in Proofs_Miscellaneous]
NoConstraint [module, in Typing]
no_method_overriding [definition, in WellFormedness]
no_method_overriding_proof [lemma, in Proofs_Miscellaneous]
no_type_overriding [definition, in WellFormedness]
no_type_overriding_proof [lemma, in Proofs_Miscellaneous]
O
Owner [inductive, in Typing]
Owner_class [constructor, in Typing]
Owner_root [constructor, in Typing]
P
parameters_as_lists [lemma, in WellFormedness]
parameters_as_lists1 [lemma, in WellFormedness]
parameters_as_lists2 [lemma, in WellFormedness]
paramOwner [axiom, in Calculus]
ParamSet [definition, in Typing]
paramset_add [definition, in Typing]
paramset_In [definition, in Typing]
paramset_union [definition, in Typing]
paramSubst_in_fieldTermList [definition, in Substitutions]
paramSubst_in_paramTermList [definition, in Substitutions]
paramSubst_in_path [definition, in Substitutions]
paramSubst_in_term [definition, in Substitutions]
paramSubst_in_type [definition, in Substitutions]
ParamSym [axiom, in Calculus]
ParamSym_eq [axiom, in Calculus]
params_evaluated [definition, in Proofs_Progress]
params_of_paramTermList [definition, in Typing]
params_of_paramTypeList [definition, in Proofs_SubstitutionLemmas2]
params_of_paramValueList [definition, in Proofs_SubstitutionLemmas2]
ParamTermList [inductive, in Calculus]
ParamTermListTyping [inductive, in Typing]
ParamTermListTyping_cons [constructor, in Typing]
ParamTermListTyping_nil [constructor, in Typing]
ParamTerm_cons [constructor, in Calculus]
ParamTerm_nil [constructor, in Calculus]
paramType [axiom, in Calculus]
ParamTypeList [definition, in Typing]
paramTypeList_to_paramList [definition, in Proofs_Miscellaneous]
ParamValueList [definition, in Subclassing]
ParamValueListTyping [inductive, in Proofs_SubjectReduction]
ParamValueListTyping_cons [constructor, in Proofs_SubjectReduction]
ParamValueListTyping_nil [constructor, in Proofs_SubjectReduction]
paramValueList_to_paramList [definition, in Proofs_Miscellaneous]
paramValueList_to_ParamTermList [definition, in Substitutions]
param_in_classEnv [lemma, in Proofs_Miscellaneous]
param_in_path [definition, in Typing]
param_in_term [definition, in Typing]
param_in_type [definition, in Typing]
param_types_are_well_formed [lemma, in Proofs_Miscellaneous]
Path [inductive, in Calculus]
PathTyping [inductive, in Typing]
Path_eqdec [lemma, in Proofs_Miscellaneous]
path_in_classEnv [lemma, in Proofs_Miscellaneous]
path_is_var_closed [definition, in DeBruijn]
path_is_var_closed' [definition, in DeBruijn]
path_is_var_closed_eq_l [lemma, in DeBruijn]
path_is_var_closed_eq_r [lemma, in DeBruijn]
Path_param [constructor, in Calculus]
Path_this [constructor, in Calculus]
path_to_term [definition, in Subclassing]
path_to_term_call [lemma, in Subclassing]
path_to_term_let [lemma, in Subclassing]
path_to_term_new [lemma, in Subclassing]
path_to_term_param [lemma, in Subclassing]
path_to_term_select [lemma, in Subclassing]
path_to_term_this [lemma, in Subclassing]
path_to_term_var [lemma, in Subclassing]
Path_value [constructor, in Calculus]
Path_var [constructor, in Calculus]
plus_minus_assoc [lemma, in Util]
polySubst_in_fieldTermCons [lemma, in Substitutions]
polySubst_in_fieldTermNil [lemma, in Substitutions]
polySubst_in_paramTermCons [lemma, in Substitutions]
polySubst_in_paramTermNil [lemma, in Substitutions]
polySubst_in_pathParam [lemma, in Substitutions]
polySubst_in_pathParam_corollary [lemma, in Substitutions]
polySubst_in_pathThis [lemma, in Substitutions]
polySubst_in_pathValue [lemma, in Substitutions]
polySubst_in_pathVar [lemma, in Substitutions]
polySubst_in_termCall [lemma, in Substitutions]
polySubst_in_termLet [lemma, in Substitutions]
polySubst_in_termNew [lemma, in Substitutions]
polySubst_in_termParam [lemma, in Substitutions]
polySubst_in_termParam_corollary [lemma, in Substitutions]
polySubst_in_termSelect [lemma, in Substitutions]
polySubst_in_termThis [lemma, in Substitutions]
polySubst_in_termValue [lemma, in Substitutions]
polySubst_in_termValue_prop1 [definition, in Substitutions]
polySubst_in_termValue_prop2 [definition, in Substitutions]
polySubst_in_termVar [lemma, in Substitutions]
polySubst_in_typeClass [lemma, in Substitutions]
polySubst_in_typeVirtual [lemma, in Substitutions]
Program [module, in Calculus]
program_is_well_formed_proof [axiom, in Proofs_Miscellaneous]
Proofs_AdmissibilityOfTransitivity [library]
Proofs_DeBruijnSIndices [library]
Proofs_Miscellaneous [library]
Proofs_Progress [library]
Proofs_Soundness [library]
Proofs_Subclassing [library]
Proofs_SubjectReduction [library]
Proofs_SubstitutionLemmas [library]
Proofs_SubstitutionLemmas2 [library]
Proofs_SubstitutionLemmas3 [library]
Proofs_TypeOrdering [library]
P_Param [constructor, in Typing]
P_This [constructor, in Typing]
P_Value [constructor, in Typing]
P_Var [constructor, in Typing]
R
Red_fieldTermList [inductive, in Semantics]
Red_paramTermList [inductive, in Semantics]
Red_term [inductive, in Semantics]
Red_term_star [definition, in Proofs_Soundness]
rootEnv [definition, in Typing]
R_Arg [constructor, in Semantics]
R_Call [constructor, in Semantics]
R_Field [constructor, in Semantics]
R_FieldTermList_head [constructor, in Semantics]
R_FieldTermList_tail [constructor, in Semantics]
R_Let [constructor, in Semantics]
R_Local [constructor, in Semantics]
R_ParamTermList_head [constructor, in Semantics]
R_ParamTermList_tail [constructor, in Semantics]
R_Select [constructor, in Semantics]
S
SC_Class [constructor, in Subclassing]
SC_Extends [constructor, in Subclassing]
Semantics [library]
SetProgram [module, in Proofs_TypeOrdering]
SetProgram [module, in Proofs_SubjectReduction]
SetProgram [module, in Proofs_SubstitutionLemmas2]
SetProgram [module, in Proofs_Miscellaneous]
SetProgram [module, in Semantics]
SetProgram [module, in Proofs_DeBruijnSIndices]
SetProgram [module, in TypeOrdering]
SetProgram [module, in Proofs_SubstitutionLemmas3]
SetProgram [module, in Proofs_Soundness]
SetProgram [module, in Proofs_Progress]
SetProgram [module, in WellFormedness]
SetProgram [module, in Typing]
SetProgram [module, in Proofs_AdmissibilityOfTransitivity]
SetProgram [module, in Proofs_Subclassing]
SetProgram [module, in Subclassing]
SetProgram [module, in Substitutions]
SetProgram [module, in Proofs_SubstitutionLemmas]
SetProgram [module, in DeBruijn]
Sid [module, in Proofs_TypeOrdering]
sid_theoryA [lemma, in Proofs_TypeOrdering]
StructuredTypingRelations [module, in Typing]
Subclass [inductive, in Subclassing]
Subclassing [library]
Substitutions [library]
Subtyping [inductive, in Typing]
Sym [definition, in Calculus]
SymbolConstraint [module, in Typing]
symbol_of_type [definition, in TypeOrdering]
symRel [axiom, in Calculus]
symRel_is_well_founded [definition, in WellFormedness]
symRel_is_well_founded_proof [lemma, in Proofs_Miscellaneous]
S_Alias_Left [constructor, in Typing]
S_Alias_Right [constructor, in Typing]
S_Class [constructor, in Typing]
S_Down [constructor, in Typing]
S_Extends [constructor, in Typing]
S_Trans [constructor, in Typing]
S_Up [constructor, in Typing]
S_Virtual [constructor, in Typing]
T
Term [inductive, in Calculus]
Term_call [constructor, in Calculus]
term_evaluated [definition, in Subclassing]
term_is_var_closed [definition, in DeBruijn]
term_is_var_closed' [definition, in DeBruijn]
Term_loc [constructor, in Calculus]
Term_new [constructor, in Calculus]
Term_param [constructor, in Calculus]
Term_select [constructor, in Calculus]
Term_this [constructor, in Calculus]
Term_var [constructor, in Calculus]
thisSubst_in_fieldTermList [definition, in Substitutions]
thisSubst_in_paramTermList [definition, in Substitutions]
thisSubst_in_paramTypeList [definition, in Proofs_SubstitutionLemmas]
thisSubst_in_path [definition, in Substitutions]
thisSubst_in_term [definition, in Substitutions]
thisSubst_in_type [definition, in Substitutions]
thisSubst_in_typeList [definition, in Proofs_SubstitutionLemmas]
this_in_path [definition, in Typing]
this_in_type [definition, in Typing]
TransitivityConstraint [module, in Typing]
type [inductive, in Calculus]
typeDefs_are_well_formed [definition, in WellFormedness]
TypeList [definition, in Typing]
TypeList_at [inductive, in Typing]
typeList_at_append [lemma, in Typing]
typeList_at_cons [lemma, in Typing]
typeList_at_elim [lemma, in Typing]
TypeList_at_head [constructor, in Typing]
typeList_at_head [lemma, in Typing]
typeList_at_intro [lemma, in Typing]
typeList_at_map [lemma, in Typing]
TypeList_at_tail [constructor, in Typing]
typeLowerBound [axiom, in Calculus]
typeLowerBounds_are_well_formed [lemma, in Proofs_Miscellaneous]
TypeOrdering [library]
typeOwner [axiom, in Calculus]
typeRel [definition, in TypeOrdering]
typeRelMul [definition, in Proofs_TypeOrdering]
typeRelMul1 [lemma, in Proofs_TypeOrdering]
typeRelMul2 [lemma, in Proofs_TypeOrdering]
typeRelMul3 [lemma, in Proofs_TypeOrdering]
typeRelMul4 [lemma, in Proofs_TypeOrdering]
typeRel_is_fun_extension [lemma, in Proofs_TypeOrdering]
TypeSym [axiom, in Calculus]
TypeSym_eq [axiom, in Calculus]
typeUpperBound [axiom, in Calculus]
typeUpperBounds_are_well_formed [lemma, in Proofs_Miscellaneous]
typeVals_are_well_formed [definition, in WellFormedness]
typeValue [axiom, in Calculus]
typeValues_are_well_formed [lemma, in Proofs_Miscellaneous]
typeVal_subtype_of_upperBound [lemma, in Proofs_Miscellaneous]
typeVal_supertype_of_lowerBound [lemma, in Proofs_Miscellaneous]
type_class [constructor, in Calculus]
Type_eqdec [lemma, in Proofs_Miscellaneous]
Type_Eqset [module, in Proofs_TypeOrdering]
Type_Eqset_dec [module, in Proofs_TypeOrdering]
type_is_closed [definition, in Typing]
type_is_var_closed [definition, in DeBruijn]
type_is_var_closed' [definition, in DeBruijn]
type_is_var_closed_eq_l [lemma, in DeBruijn]
type_is_var_closed_eq_r [lemma, in DeBruijn]
Type_Multiset [module, in Proofs_TypeOrdering]
Type_MultisetOrder [module, in Proofs_TypeOrdering]
type_virtual [constructor, in Calculus]
Typing [inductive, in Typing]
Typing [library]
TypingRelations [module, in Typing]
T_Call [constructor, in Typing]
T_Let [constructor, in Typing]
T_New [constructor, in Typing]
T_Param [constructor, in Typing]
T_Select [constructor, in Typing]
T_This [constructor, in Typing]
T_Var [constructor, in Typing]
U
Util [library]
V
Value [inductive, in Calculus]
ValueList [definition, in Subclassing]
values [inductive, in Typing]
values [inductive, in Typing]
values [inductive, in Typing]
values [inductive, in Typing]
Value_eqdec [lemma, in Proofs_Miscellaneous]
Value_eqdec' [definition, in Proofs_Miscellaneous]
Value_mk [constructor, in Calculus]
value_to_term [definition, in Subclassing]
VarSet [definition, in DeBruijn]
varset_add [definition, in DeBruijn]
varset_In [definition, in DeBruijn]
varset_union [definition, in DeBruijn]
varSubst_in_fieldTermList [definition, in Substitutions]
varSubst_in_paramTermList [definition, in Substitutions]
varSubst_in_path [definition, in Substitutions]
varSubst_in_term [definition, in Substitutions]
varSubst_in_type [definition, in Substitutions]
VarSym [definition, in Calculus]
VarSym_eqdec [lemma, in Subclassing]
var_in_classEnv [lemma, in Proofs_Miscellaneous]
var_in_path [definition, in DeBruijn]
var_in_term [definition, in DeBruijn]
var_in_type [definition, in DeBruijn]
W
WellFormedness [library]
WellFoundation [library]
well_foundation1 [lemma, in WellFoundation]
well_foundation2 [lemma, in WellFoundation]
well_foundation3 [lemma, in WellFoundation]
well_foundation4 [lemma, in WellFoundation]
WF_class [inductive, in WellFormedness]
WF_class_intro [constructor, in WellFormedness]
WF_fieldDef [inductive, in WellFormedness]
WF_fieldDef_intro [constructor, in WellFormedness]
WF_methodDef [inductive, in WellFormedness]
WF_methodDef_intro [constructor, in WellFormedness]
WF_methodVal [inductive, in WellFormedness]
WF_methodVal_intro [constructor, in WellFormedness]
WF_program [inductive, in WellFormedness]
WF_program_intro [constructor, in WellFormedness]
WF_typeDef [inductive, in WellFormedness]
WF_typeDef_intro [constructor, in WellFormedness]
WF_typeVal [inductive, in WellFormedness]
WF_typeVal_intro [constructor, in WellFormedness]
X
xT [constructor, in Proofs_SubstitutionLemmas]
Z
zero_fv_and_varSubst_0 [lemma, in Proofs_SubstitutionLemmas3]
zero_fv_and_varSubst_2 [lemma, in Proofs_SubstitutionLemmas3]
Axiom Index
A
applyTo [in Typing]
C
classSuper [in Calculus]
ClassSym [in Calculus]
ClassSym_eq [in Calculus]
F
fieldOwner [in Calculus]
FieldSym [in Calculus]
FieldSym_eq [in Calculus]
fieldType [in Calculus]
M
main [in Calculus]
methodOwner [in Calculus]
MethodSym [in Calculus]
MethodSym_eq [in Calculus]
methodType [in Calculus]
methodValue [in Calculus]
method_parameters_spec [in Calculus]
P
paramOwner [in Calculus]
ParamSym [in Calculus]
ParamSym_eq [in Calculus]
paramType [in Calculus]
program_is_well_formed_proof [in Proofs_Miscellaneous]
S
symRel [in Calculus]
T
typeLowerBound [in Calculus]
typeOwner [in Calculus]
TypeSym [in Calculus]
TypeSym_eq [in Calculus]
typeUpperBound [in Calculus]
typeValue [in Calculus]
Lemma Index
C
classes_are_well_formed_proof [in Proofs_Miscellaneous]
classes_smaller_than_types_proof [in Proofs_Miscellaneous]
cons_destruct [in Util]
E
empty_is_empty_1 [in Util]
empty_is_empty_2 [in Util]
empty_union_left [in Util]
empty_union_right [in Util]
F
fieldTypes_are_well_formed [in Proofs_Miscellaneous]
forall_is_listForall [in Proofs_SubstitutionLemmas]
fp_and_paramSubst_in_path [in Proofs_Miscellaneous]
fp_and_paramSubst_in_type [in Proofs_Miscellaneous]
free_parameters_and_lifting_aux_0 [in Proofs_Miscellaneous]
free_parameters_and_lifting_aux_2 [in Proofs_Miscellaneous]
free_parameters_and_lifting_0 [in Proofs_Miscellaneous]
free_parameters_and_lifting_2 [in Proofs_Miscellaneous]
fv_and_paramSubst_in_path [in Proofs_Miscellaneous]
fv_and_paramSubst_in_type [in Proofs_Miscellaneous]
fv_and_thisSubst_in_path [in DeBruijn]
fv_and_thisSubst_in_type [in DeBruijn]
fv_and_var_in_path [in DeBruijn]
fv_and_var_in_path1 [in DeBruijn]
fv_and_var_in_path2 [in DeBruijn]
fv_and_var_in_type [in DeBruijn]
fv_and_var_in_type1 [in DeBruijn]
fv_and_var_in_type2 [in DeBruijn]
fv_pathvar_empty [in DeBruijn]
fv_pathvar_non_empty [in DeBruijn]
fv_termvar_empty [in DeBruijn]
fv_termvar_non_empty [in DeBruijn]
L
lemmaA1 [in Proofs_Miscellaneous]
lemmaA10_0 [in Proofs_Miscellaneous]
lemmaA10_2 [in Proofs_Miscellaneous]
lemmaA12 [in Proofs_TypeOrdering]
lemmaA12' [in Proofs_TypeOrdering]
lemmaA13_1 [in Proofs_TypeOrdering]
lemmaA13_1' [in Proofs_TypeOrdering]
lemmaA13_2 [in Proofs_TypeOrdering]
lemmaA13_3 [in Proofs_TypeOrdering]
lemmaA14 [in Proofs_TypeOrdering]
lemmaA15_1 [in Proofs_TypeOrdering]
lemmaA15_2 [in Proofs_TypeOrdering]
lemmaA17 [in Proofs_TypeOrdering]
lemmaA18 [in Proofs_TypeOrdering]
lemmaA18_aux_1 [in Proofs_TypeOrdering]
lemmaA18_aux_2 [in Proofs_TypeOrdering]
lemmaA19 [in Proofs_Subclassing]
lemmaA1_for_paths [in Proofs_SubstitutionLemmas]
lemmaA20 [in Proofs_Subclassing]
lemmaA21 [in Proofs_Subclassing]
lemmaA21_aux [in Proofs_Subclassing]
lemmaA22 [in Proofs_Subclassing]
lemmaA23_1 [in Proofs_AdmissibilityOfTransitivity]
lemmaA23_2 [in Proofs_AdmissibilityOfTransitivity]
lemmaA24_aux [in Proofs_Miscellaneous]
lemmaA24_2 [in Proofs_AdmissibilityOfTransitivity]
lemmaA24_2_aux [in Proofs_AdmissibilityOfTransitivity]
lemmaA25 [in Proofs_AdmissibilityOfTransitivity]
lemmaA26_1 [in Proofs_AdmissibilityOfTransitivity]
lemmaA26_1_aux [in Proofs_AdmissibilityOfTransitivity]
lemmaA26_2 [in Proofs_AdmissibilityOfTransitivity]
lemmaA26_2_aux [in Proofs_AdmissibilityOfTransitivity]
lemmaA27 [in Proofs_AdmissibilityOfTransitivity]
lemmaA28_1 [in Proofs_AdmissibilityOfTransitivity]
lemmaA28_2 [in Proofs_AdmissibilityOfTransitivity]
lemmaA29 [in Proofs_Progress]
lemmaA29_aux_1 [in Proofs_Progress]
lemmaA29_aux_2 [in Proofs_Progress]
lemmaA29_aux_3 [in Proofs_Progress]
lemmaA2_1 [in Proofs_Miscellaneous]
lemmaA2_2 [in Proofs_Miscellaneous]
lemmaA30_0 [in Proofs_DeBruijnSIndices]
lemmaA30_0' [in Proofs_DeBruijnSIndices]
lemmaA30_1 [in Proofs_DeBruijnSIndices]
lemmaA30_1' [in Proofs_DeBruijnSIndices]
lemmaA30_2 [in Proofs_DeBruijnSIndices]
lemmaA30_2' [in Proofs_DeBruijnSIndices]
lemmaA31_0 [in Proofs_DeBruijnSIndices]
lemmaA31_0' [in Proofs_DeBruijnSIndices]
lemmaA31_1 [in Proofs_DeBruijnSIndices]
lemmaA31_1' [in Proofs_DeBruijnSIndices]
lemmaA31_2 [in Proofs_DeBruijnSIndices]
lemmaA31_2' [in Proofs_DeBruijnSIndices]
lemmaA32 [in Proofs_DeBruijnSIndices]
lemmaA33_0 [in Proofs_DeBruijnSIndices]
lemmaA33_0' [in Proofs_DeBruijnSIndices]
lemmaA33_1 [in Proofs_DeBruijnSIndices]
lemmaA33_1' [in Proofs_DeBruijnSIndices]
lemmaA33_2 [in Proofs_DeBruijnSIndices]
lemmaA33_2' [in Proofs_DeBruijnSIndices]
lemmaA34_0 [in Proofs_DeBruijnSIndices]
lemmaA34_0' [in Proofs_DeBruijnSIndices]
lemmaA34_1 [in Proofs_DeBruijnSIndices]
lemmaA34_1' [in Proofs_DeBruijnSIndices]
lemmaA34_2 [in Proofs_DeBruijnSIndices]
lemmaA34_2' [in Proofs_DeBruijnSIndices]
lemmaA35_0 [in Proofs_DeBruijnSIndices]
lemmaA35_0' [in Proofs_DeBruijnSIndices]
lemmaA35_1 [in Proofs_DeBruijnSIndices]
lemmaA35_1' [in Proofs_DeBruijnSIndices]
lemmaA35_2 [in Proofs_DeBruijnSIndices]
lemmaA35_2' [in Proofs_DeBruijnSIndices]
lemmaA36_32 [in Proofs_DeBruijnSIndices]
lemmaA36_33_0 [in Proofs_DeBruijnSIndices]
lemmaA36_33_0' [in Proofs_DeBruijnSIndices]
lemmaA36_33_1 [in Proofs_DeBruijnSIndices]
lemmaA36_33_1' [in Proofs_DeBruijnSIndices]
lemmaA36_33_2 [in Proofs_DeBruijnSIndices]
lemmaA36_33_2' [in Proofs_DeBruijnSIndices]
lemmaA36_34_0 [in Proofs_DeBruijnSIndices]
lemmaA36_34_0' [in Proofs_DeBruijnSIndices]
lemmaA36_34_1 [in Proofs_DeBruijnSIndices]
lemmaA36_34_1' [in Proofs_DeBruijnSIndices]
lemmaA36_34_2 [in Proofs_DeBruijnSIndices]
lemmaA36_34_2' [in Proofs_DeBruijnSIndices]
lemmaA36_35_0 [in Proofs_DeBruijnSIndices]
lemmaA36_35_0' [in Proofs_DeBruijnSIndices]
lemmaA36_35_1 [in Proofs_DeBruijnSIndices]
lemmaA36_35_1' [in Proofs_DeBruijnSIndices]
lemmaA36_35_2 [in Proofs_DeBruijnSIndices]
lemmaA36_35_2' [in Proofs_DeBruijnSIndices]
lemmaA37_0 [in Proofs_DeBruijnSIndices]
lemmaA37_0' [in Proofs_DeBruijnSIndices]
lemmaA37_1 [in Proofs_DeBruijnSIndices]
lemmaA37_1' [in Proofs_DeBruijnSIndices]
lemmaA37_2 [in Proofs_DeBruijnSIndices]
lemmaA37_2' [in Proofs_DeBruijnSIndices]
lemmaA38_0 [in Proofs_SubstitutionLemmas]
lemmaA38_0_corollary [in Proofs_SubstitutionLemmas]
lemmaA38_2 [in Proofs_SubstitutionLemmas]
lemmaA39_param_aux_1 [in Proofs_SubstitutionLemmas2]
lemmaA39_param_aux_2 [in Proofs_SubstitutionLemmas2]
lemmaA39_param_aux_3 [in Proofs_SubstitutionLemmas2]
lemmaA39_param_aux_4 [in Proofs_SubstitutionLemmas2]
lemmaA39_param_aux_4_corollary [in Proofs_SubstitutionLemmas2]
lemmaA39_param_main [in Proofs_SubstitutionLemmas2]
lemmaA39_param_0 [in Proofs_SubstitutionLemmas2]
lemmaA39_param_1 [in Proofs_SubstitutionLemmas2]
lemmaA39_param_2 [in Proofs_SubstitutionLemmas2]
lemmaA39_this1_aux_1 [in Proofs_SubstitutionLemmas]
lemmaA39_this1_aux_2 [in Proofs_SubstitutionLemmas]
lemmaA39_this_main [in Proofs_SubstitutionLemmas]
lemmaA39_this_0 [in Proofs_SubstitutionLemmas]
lemmaA39_this_1 [in Proofs_SubstitutionLemmas]
lemmaA39_this_2 [in Proofs_SubstitutionLemmas]
lemmaA39_var_aux_1 [in Proofs_SubstitutionLemmas3]
lemmaA39_var_aux_2 [in Proofs_SubstitutionLemmas3]
lemmaA39_var_aux_3 [in Proofs_SubstitutionLemmas3]
lemmaA39_var_aux_4 [in Proofs_SubstitutionLemmas3]
lemmaA39_var_aux_5 [in Proofs_SubstitutionLemmas3]
lemmaA39_var_aux_6 [in Proofs_SubstitutionLemmas3]
lemmaA39_var_aux_7 [in Proofs_SubstitutionLemmas3]
lemmaA39_var_aux_8 [in Proofs_SubstitutionLemmas3]
lemmaA39_var_main [in Proofs_SubstitutionLemmas3]
lemmaA39_var_0 [in Proofs_SubstitutionLemmas3]
lemmaA39_var_1 [in Proofs_SubstitutionLemmas3]
lemmaA39_var_1_corollary [in Proofs_SubstitutionLemmas3]
lemmaA39_var_2 [in Proofs_SubstitutionLemmas3]
lemmaA3_aux_1 [in Proofs_Miscellaneous]
lemmaA3_0 [in Proofs_Miscellaneous]
lemmaA3_2 [in Proofs_Miscellaneous]
lemmaA3_3 [in Proofs_Miscellaneous]
lemmaA3_3_corollary [in Proofs_Miscellaneous]
lemmaA40 [in Proofs_SubjectReduction]
lemmaA40_aux_1 [in Proofs_SubjectReduction]
lemmaA40_aux_10 [in Proofs_SubstitutionLemmas]
lemmaA40_aux_11 [in Proofs_SubjectReduction]
lemmaA40_aux_12 [in Proofs_SubjectReduction]
lemmaA40_aux_13 [in Proofs_SubjectReduction]
lemmaA40_aux_14 [in Proofs_SubjectReduction]
lemmaA40_aux_15 [in Proofs_SubjectReduction]
lemmaA40_aux_16 [in Proofs_SubjectReduction]
lemmaA40_aux_2 [in Proofs_SubjectReduction]
lemmaA40_aux_3 [in Proofs_SubjectReduction]
lemmaA40_aux_4 [in Proofs_SubstitutionLemmas]
lemmaA40_aux_5 [in Proofs_SubjectReduction]
lemmaA40_aux_6 [in Proofs_SubjectReduction]
lemmaA40_aux_7 [in Proofs_SubjectReduction]
lemmaA40_aux_8 [in Proofs_SubstitutionLemmas]
lemmaA40_aux_9 [in Proofs_SubstitutionLemmas]
lemmaA41 [in Proofs_Soundness]
lemmaA42 [in Proofs_Soundness]
lemmaA4_0 [in Proofs_Miscellaneous]
lemmaA4_0' [in Proofs_Miscellaneous]
lemmaA4_0_corollary [in Proofs_Miscellaneous]
lemmaA4_1 [in Proofs_Miscellaneous]
lemmaA4_2 [in Proofs_Miscellaneous]
lemmaA4_2' [in Proofs_Miscellaneous]
lemmaA4_3 [in Proofs_Miscellaneous]
lemmaA4_3' [in Proofs_Miscellaneous]
lemmaA4_3_corollary [in Proofs_Miscellaneous]
lemmaA5 [in Proofs_Miscellaneous]
lemmaA6_1 [in Proofs_Miscellaneous]
lemmaA6_1' [in Proofs_Miscellaneous]
lemmaA6_2 [in Proofs_Miscellaneous]
lemmaA6_2' [in Proofs_Miscellaneous]
lemmaA6_3 [in Proofs_Miscellaneous]
lemmaA6_3' [in Proofs_Miscellaneous]
lemmaA7 [in Proofs_Miscellaneous]
lemmaA7' [in Proofs_Miscellaneous]
lemmaA8_1 [in Proofs_Miscellaneous]
lemmaA8_2 [in Proofs_Miscellaneous]
lemmaA9_aux_0 [in Proofs_Miscellaneous]
lemmaA9_0 [in Proofs_Miscellaneous]
lemmaA9_2 [in Proofs_Miscellaneous]
length_of_append [in Util]
length_of_map [in Util]
listForall_is_forall [in Proofs_SubstitutionLemmas]
M
main_term_is_well_typed [in Proofs_Miscellaneous]
map_elim [in Util]
map_intro [in Util]
map_of_append [in Util]
Match2 [in MatchCompNat]
Match2_diff [in MatchCompNat]
Match3 [in MatchCompNat]
Match3_diff [in MatchCompNat]
match_comp_nat2_aux_0 [in MatchCompNat]
match_comp_nat2_aux_1 [in MatchCompNat]
match_comp_nat2_aux_2 [in MatchCompNat]
match_comp_nat2_ge [in MatchCompNat]
match_comp_nat2_lt [in MatchCompNat]
match_comp_nat3_aux_1 [in MatchCompNat]
match_comp_nat3_aux_2 [in MatchCompNat]
match_comp_nat3_aux_3 [in MatchCompNat]
match_comp_nat3_eq [in MatchCompNat]
match_comp_nat3_gt [in MatchCompNat]
match_comp_nat3_lt [in MatchCompNat]
methodBody_of_type_methodType [in Proofs_Miscellaneous]
methodTypes_are_well_formed [in Proofs_Miscellaneous]
myarith_1 [in Util]
myarith_2 [in Util]
N
new_lemma1_0 [in Proofs_Miscellaneous]
new_lemma1_2 [in Proofs_Miscellaneous]
new_lemma2_0 [in Proofs_Miscellaneous]
new_lemma2_2 [in Proofs_Miscellaneous]
no_method_overriding_proof [in Proofs_Miscellaneous]
no_type_overriding_proof [in Proofs_Miscellaneous]
P
parameters_as_lists [in WellFormedness]
parameters_as_lists1 [in WellFormedness]
parameters_as_lists2 [in WellFormedness]
param_in_classEnv [in Proofs_Miscellaneous]
param_types_are_well_formed [in Proofs_Miscellaneous]
Path_eqdec [in Proofs_Miscellaneous]
path_in_classEnv [in Proofs_Miscellaneous]
path_is_var_closed_eq_l [in DeBruijn]
path_is_var_closed_eq_r [in DeBruijn]
path_to_term_call [in Subclassing]
path_to_term_let [in Subclassing]
path_to_term_new [in Subclassing]
path_to_term_param [in Subclassing]
path_to_term_select [in Subclassing]
path_to_term_this [in Subclassing]
path_to_term_var [in Subclassing]
plus_minus_assoc [in Util]
polySubst_in_fieldTermCons [in Substitutions]
polySubst_in_fieldTermNil [in Substitutions]
polySubst_in_paramTermCons [in Substitutions]
polySubst_in_paramTermNil [in Substitutions]
polySubst_in_pathParam [in Substitutions]
polySubst_in_pathParam_corollary [in Substitutions]
polySubst_in_pathThis [in Substitutions]
polySubst_in_pathValue [in Substitutions]
polySubst_in_pathVar [in Substitutions]
polySubst_in_termCall [in Substitutions]
polySubst_in_termLet [in Substitutions]
polySubst_in_termNew [in Substitutions]
polySubst_in_termParam [in Substitutions]
polySubst_in_termParam_corollary [in Substitutions]
polySubst_in_termSelect [in Substitutions]
polySubst_in_termThis [in Substitutions]
polySubst_in_termValue [in Substitutions]
polySubst_in_termVar [in Substitutions]
polySubst_in_typeClass [in Substitutions]
polySubst_in_typeVirtual [in Substitutions]
S
sid_theoryA [in Proofs_TypeOrdering]
symRel_is_well_founded_proof [in Proofs_Miscellaneous]
T
typeList_at_append [in Typing]
typeList_at_cons [in Typing]
typeList_at_elim [in Typing]
typeList_at_head [in Typing]
typeList_at_intro [in Typing]
typeList_at_map [in Typing]
typeLowerBounds_are_well_formed [in Proofs_Miscellaneous]
typeRelMul1 [in Proofs_TypeOrdering]
typeRelMul2 [in Proofs_TypeOrdering]
typeRelMul3 [in Proofs_TypeOrdering]
typeRelMul4 [in Proofs_TypeOrdering]
typeRel_is_fun_extension [in Proofs_TypeOrdering]
typeUpperBounds_are_well_formed [in Proofs_Miscellaneous]
typeValues_are_well_formed [in Proofs_Miscellaneous]
typeVal_subtype_of_upperBound [in Proofs_Miscellaneous]
typeVal_supertype_of_lowerBound [in Proofs_Miscellaneous]
Type_eqdec [in Proofs_Miscellaneous]
type_is_var_closed_eq_l [in DeBruijn]
type_is_var_closed_eq_r [in DeBruijn]
V
Value_eqdec [in Proofs_Miscellaneous]
VarSym_eqdec [in Subclassing]
var_in_classEnv [in Proofs_Miscellaneous]
W
well_foundation1 [in WellFoundation]
well_foundation2 [in WellFoundation]
well_foundation3 [in WellFoundation]
well_foundation4 [in WellFoundation]
Z
zero_fv_and_varSubst_0 [in Proofs_SubstitutionLemmas3]
zero_fv_and_varSubst_2 [in Proofs_SubstitutionLemmas3]
Constructor Index
C
context_is_well_formed_intro [in Proofs_SubstitutionLemmas]
E
Env_mk [in Typing]
Evaluate_end [in Semantics]
Evaluate_step [in Semantics]
F
FieldTermListTyping_cons [in Typing]
FieldTermListTyping_nil [in Typing]
FieldTerm_cons [in Calculus]
FieldTerm_nil [in Calculus]
FieldValueListTyping_cons [in Typing]
FieldValueListTyping_nil [in Typing]
FieldValueList_contains_head [in Subclassing]
FieldValueList_contains_tail [in Subclassing]
FieldValue_cons [in Calculus]
FieldValue_nil [in Calculus]
G
Gen_FieldValueListTyping_cons [in Typing]
Gen_FieldValueListTyping_nil [in Typing]
Gen_P_Param [in Typing]
Gen_P_This [in Typing]
Gen_P_Value [in Typing]
Gen_P_Var [in Typing]
Gen_S_Alias_Left [in Typing]
Gen_S_Alias_Right [in Typing]
Gen_S_Class [in Typing]
Gen_S_Down [in Typing]
Gen_S_Extends [in Typing]
Gen_S_Trans [in Typing]
Gen_S_Up [in Typing]
Gen_S_Virtual [in Typing]
I
IsComplete_intro [in Typing]
K
K_Class [in WellFormedness]
K_Virtual [in WellFormedness]
O
Owner_class [in Typing]
Owner_root [in Typing]
P
ParamTermListTyping_cons [in Typing]
ParamTermListTyping_nil [in Typing]
ParamTerm_cons [in Calculus]
ParamTerm_nil [in Calculus]
ParamValueListTyping_cons [in Proofs_SubjectReduction]
ParamValueListTyping_nil [in Proofs_SubjectReduction]
Path_param [in Calculus]
Path_this [in Calculus]
Path_value [in Calculus]
Path_var [in Calculus]
P_Param [in Typing]
P_This [in Typing]
P_Value [in Typing]
P_Var [in Typing]
R
R_Arg [in Semantics]
R_Call [in Semantics]
R_Field [in Semantics]
R_FieldTermList_head [in Semantics]
R_FieldTermList_tail [in Semantics]
R_Let [in Semantics]
R_Local [in Semantics]
R_ParamTermList_head [in Semantics]
R_ParamTermList_tail [in Semantics]
R_Select [in Semantics]
S
SC_Class [in Subclassing]
SC_Extends [in Subclassing]
S_Alias_Left [in Typing]
S_Alias_Right [in Typing]
S_Class [in Typing]
S_Down [in Typing]
S_Extends [in Typing]
S_Trans [in Typing]
S_Up [in Typing]
S_Virtual [in Typing]
T
Term_call [in Calculus]
Term_loc [in Calculus]
Term_new [in Calculus]
Term_param [in Calculus]
Term_select [in Calculus]
Term_this [in Calculus]
Term_var [in Calculus]
TypeList_at_head [in Typing]
TypeList_at_tail [in Typing]
type_class [in Calculus]
type_virtual [in Calculus]
T_Call [in Typing]
T_Let [in Typing]
T_New [in Typing]
T_Param [in Typing]
T_Select [in Typing]
T_This [in Typing]
T_Var [in Typing]
V
Value_mk [in Calculus]
W
WF_class_intro [in WellFormedness]
WF_fieldDef_intro [in WellFormedness]
WF_methodDef_intro [in WellFormedness]
WF_methodVal_intro [in WellFormedness]
WF_program_intro [in WellFormedness]
WF_typeDef_intro [in WellFormedness]
WF_typeVal_intro [in WellFormedness]
X
xT [in Proofs_SubstitutionLemmas]
Inductive Index
C
context_is_well_formed [in Proofs_SubstitutionLemmas]
E
Env [in Typing]
Evaluate [in Semantics]
F
FieldTermList [in Calculus]
FieldTermListTyping [in Typing]
FieldValueList [in Calculus]
FieldValueListTyping [in Typing]
FieldValueList_contains [in Subclassing]
G
Gen_FieldValueListTyping [in Typing]
Gen_PathTyping [in Typing]
Gen_Subtyping [in Typing]
I
IsComplete [in Typing]
K
Kinding [in WellFormedness]
O
Owner [in Typing]
P
ParamTermList [in Calculus]
ParamTermListTyping [in Typing]
ParamValueListTyping [in Proofs_SubjectReduction]
Path [in Calculus]
PathTyping [in Typing]
R
Red_fieldTermList [in Semantics]
Red_paramTermList [in Semantics]
Red_term [in Semantics]
S
Subclass [in Subclassing]
Subtyping [in Typing]
T
Term [in Calculus]
type [in Calculus]
TypeList_at [in Typing]
Typing [in Typing]
V
Value [in Calculus]
values [in Typing]
values [in Typing]
values [in Typing]
values [in Typing]
W
WF_class [in WellFormedness]
WF_fieldDef [in WellFormedness]
WF_methodDef [in WellFormedness]
WF_methodVal [in WellFormedness]
WF_program [in WellFormedness]
WF_typeDef [in WellFormedness]
WF_typeVal [in WellFormedness]
Definition Index
A
A [in Proofs_TypeOrdering]
A [in Proofs_TypeOrdering]
amplitude [in DeBruijn]
amplitude [in DeBruijn]
amplitude [in DeBruijn]
amplitude [in DeBruijn]
applyTo [in Typing]
applyTo [in Typing]
args_are_correct [in Proofs_SubstitutionLemmas2]
args_conform_to_params [in Proofs_SubstitutionLemmas2]
C
classEnv [in Typing]
classes_are_well_formed [in WellFormedness]
classes_smaller_than_types [in WellFormedness]
D
drop_at_depth_in_fieldTermList [in DeBruijn]
drop_at_depth_in_paramTermList [in DeBruijn]
drop_at_depth_in_path [in DeBruijn]
drop_at_depth_in_term [in DeBruijn]
drop_at_depth_in_type [in DeBruijn]
drop_in_path [in DeBruijn]
drop_in_term [in DeBruijn]
drop_in_type [in DeBruijn]
E
empty_paramset [in Typing]
empty_varset [in DeBruijn]
eqA [in Proofs_TypeOrdering]
eqA [in Proofs_TypeOrdering]
eqA_dec [in Proofs_TypeOrdering]
eqA_dec [in Proofs_TypeOrdering]
EvaluateMain [in Semantics]
F
fieldDefs_are_well_formed [in WellFormedness]
fields_evaluated [in Proofs_Progress]
fields_of_fieldTermList [in Typing]
fields_of_fieldValueList [in Typing]
FieldValueList_eqdec' [in Proofs_Miscellaneous]
fieldValueList_to_fieldTermList [in Subclassing]
fp_in_fieldTermList [in Typing]
fp_in_paramTermList [in Typing]
fp_in_path [in Typing]
fp_in_term [in Typing]
fp_in_type [in Typing]
fun_extension [in WellFoundation]
fv_at_depth_in_fieldTermList [in DeBruijn]
fv_at_depth_in_paramTermList [in DeBruijn]
fv_at_depth_in_path [in DeBruijn]
fv_at_depth_in_term [in DeBruijn]
fv_at_depth_in_type [in DeBruijn]
fv_in_fieldTermList [in DeBruijn]
fv_in_paramTermList [in DeBruijn]
fv_in_path [in DeBruijn]
fv_in_term [in DeBruijn]
fv_in_type [in DeBruijn]
I
IsComplete_fields [in Typing]
IsComplete_methods [in Typing]
IsComplete_params [in Typing]
IsComplete_types [in Typing]
L
lemmaA23_prop1 [in Proofs_AdmissibilityOfTransitivity]
lemmaA23_prop2 [in Proofs_AdmissibilityOfTransitivity]
lemmaA23_prop3 [in Proofs_AdmissibilityOfTransitivity]
lemmaA24_prop_1 [in Proofs_AdmissibilityOfTransitivity]
lemmaA24_prop_2 [in Proofs_AdmissibilityOfTransitivity]
lemmaA24_prop_3 [in Proofs_AdmissibilityOfTransitivity]
lemmaA26_prop_1 [in Proofs_AdmissibilityOfTransitivity]
lemmaA26_prop_2 [in Proofs_AdmissibilityOfTransitivity]
lemmaA27_prop [in Proofs_AdmissibilityOfTransitivity]
lemmaA28_prop1 [in Proofs_AdmissibilityOfTransitivity]
lemmaA28_prop2 [in Proofs_AdmissibilityOfTransitivity]
lemmaA28_prop3 [in Proofs_AdmissibilityOfTransitivity]
lemmaA29_aux_2_prop1 [in Proofs_Progress]
lemmaA29_aux_2_prop2 [in Proofs_Progress]
lemmaA29_aux_2_prop3 [in Proofs_Progress]
lemmaA29_prop1 [in Proofs_Progress]
lemmaA29_prop2 [in Proofs_Progress]
lemmaA29_prop3 [in Proofs_Progress]
lemmaA30_1_prop1 [in Proofs_DeBruijnSIndices]
lemmaA30_1_prop2 [in Proofs_DeBruijnSIndices]
lemmaA30_1_prop3 [in Proofs_DeBruijnSIndices]
lemmaA31_1_prop1 [in Proofs_DeBruijnSIndices]
lemmaA31_1_prop2 [in Proofs_DeBruijnSIndices]
lemmaA31_1_prop3 [in Proofs_DeBruijnSIndices]
lemmaA32_prop1 [in Proofs_DeBruijnSIndices]
lemmaA32_prop2 [in Proofs_DeBruijnSIndices]
lemmaA33_1_prop1 [in Proofs_DeBruijnSIndices]
lemmaA33_1_prop2 [in Proofs_DeBruijnSIndices]
lemmaA33_1_prop3 [in Proofs_DeBruijnSIndices]
lemmaA34_1_prop1 [in Proofs_DeBruijnSIndices]
lemmaA34_1_prop2 [in Proofs_DeBruijnSIndices]
lemmaA34_1_prop3 [in Proofs_DeBruijnSIndices]
lemmaA35_1_prop1 [in Proofs_DeBruijnSIndices]
lemmaA35_1_prop2 [in Proofs_DeBruijnSIndices]
lemmaA35_1_prop3 [in Proofs_DeBruijnSIndices]
lemmaA36_32_prop1 [in Proofs_DeBruijnSIndices]
lemmaA36_32_prop2 [in Proofs_DeBruijnSIndices]
lemmaA36_33_1_prop1 [in Proofs_DeBruijnSIndices]
lemmaA36_33_1_prop2 [in Proofs_DeBruijnSIndices]
lemmaA36_33_1_prop3 [in Proofs_DeBruijnSIndices]
lemmaA36_34_1_prop1 [in Proofs_DeBruijnSIndices]
lemmaA36_34_1_prop2 [in Proofs_DeBruijnSIndices]
lemmaA36_34_1_prop3 [in Proofs_DeBruijnSIndices]
lemmaA36_35_1_prop1 [in Proofs_DeBruijnSIndices]
lemmaA36_35_1_prop2 [in Proofs_DeBruijnSIndices]
lemmaA36_35_1_prop3 [in Proofs_DeBruijnSIndices]
lemmaA37_1_prop1 [in Proofs_DeBruijnSIndices]
lemmaA37_1_prop2 [in Proofs_DeBruijnSIndices]
lemmaA37_1_prop3 [in Proofs_DeBruijnSIndices]
lemmaA38_0_prop1 [in Proofs_SubstitutionLemmas]
lemmaA38_0_prop2 [in Proofs_SubstitutionLemmas]
lemmaA38_0_prop3 [in Proofs_SubstitutionLemmas]
lemmaA39_param1_prop1 [in Proofs_SubstitutionLemmas2]
lemmaA39_param1_prop2 [in Proofs_SubstitutionLemmas2]
lemmaA39_param1_prop3 [in Proofs_SubstitutionLemmas2]
lemmaA39_param_prop1 [in Proofs_SubstitutionLemmas2]
lemmaA39_param_prop2 [in Proofs_SubstitutionLemmas2]
lemmaA39_param_prop3 [in Proofs_SubstitutionLemmas2]
lemmaA39_this1_prop1 [in Proofs_SubstitutionLemmas]
lemmaA39_this1_prop2 [in Proofs_SubstitutionLemmas]
lemmaA39_this1_prop3 [in Proofs_SubstitutionLemmas]
lemmaA39_this_prop1 [in Proofs_SubstitutionLemmas]
lemmaA39_this_prop2 [in Proofs_SubstitutionLemmas]
lemmaA39_this_prop3 [in Proofs_SubstitutionLemmas]
lemmaA39_var1_prop1 [in Proofs_SubstitutionLemmas3]
lemmaA39_var1_prop2 [in Proofs_SubstitutionLemmas3]
lemmaA39_var1_prop3 [in Proofs_SubstitutionLemmas3]
lemmaA39_var_prop1 [in Proofs_SubstitutionLemmas3]
lemmaA39_var_prop2 [in Proofs_SubstitutionLemmas3]
lemmaA39_var_prop3 [in Proofs_SubstitutionLemmas3]
lemmaA3_prop1 [in Proofs_Miscellaneous]
lemmaA3_prop2 [in Proofs_Miscellaneous]
lemmaA40_aux_4_prop1 [in Proofs_SubstitutionLemmas]
lemmaA40_aux_4_prop2 [in Proofs_SubstitutionLemmas]
lemmaA40_aux_8_prop1 [in Proofs_SubstitutionLemmas]
lemmaA40_aux_8_prop2 [in Proofs_SubstitutionLemmas]
lemmaA40_prop1 [in Proofs_SubjectReduction]
lemmaA40_prop2 [in Proofs_SubjectReduction]
lemmaA40_prop3 [in Proofs_SubjectReduction]
lemmaA4_prop1 [in Proofs_Miscellaneous]
lemmaA4_prop2 [in Proofs_Miscellaneous]
lemmaA4_1_prop1 [in Proofs_Miscellaneous]
lemmaA4_1_prop2 [in Proofs_Miscellaneous]
lemmaA4_1_prop3 [in Proofs_Miscellaneous]
lemmaA5_P1 [in Proofs_Miscellaneous]
lemmaA5_P2 [in Proofs_Miscellaneous]
lift_at_depth_in_fieldTermList [in DeBruijn]
lift_at_depth_in_paramTermList [in DeBruijn]
lift_at_depth_in_path [in DeBruijn]
lift_at_depth_in_term [in DeBruijn]
lift_at_depth_in_type [in DeBruijn]
lift_at_depth_in_var [in DeBruijn]
lift_in_path [in DeBruijn]
lift_in_term [in DeBruijn]
lift_in_type [in DeBruijn]
List_disjoint [in Typing]
list_forall [in Proofs_SubstitutionLemmas]
List_sublist [in Proofs_SubstitutionLemmas2]
local_types_well_formed [in Proofs_SubstitutionLemmas]
local_types_well_formed_aux [in Proofs_SubstitutionLemmas]
M
map_paramSubst_in_fieldTermList [in Substitutions]
map_paramSubst_in_paramTermList [in Substitutions]
map_paramSubst_in_path [in Substitutions]
map_paramSubst_in_term [in Substitutions]
map_paramSubst_in_type [in Substitutions]
map_paramSubst_in_typeList [in Proofs_SubstitutionLemmas2]
map_varSubst_in_typeList [in Proofs_SubstitutionLemmas3]
match_comp_nat2 [in MatchCompNat]
match_comp_nat3 [in MatchCompNat]
methodDefs_are_well_formed [in WellFormedness]
methodVals_are_well_formed [in WellFormedness]
method_parameters [in WellFormedness]
N
no_method_overriding [in WellFormedness]
no_type_overriding [in WellFormedness]
P
ParamSet [in Typing]
paramset_add [in Typing]
paramset_In [in Typing]
paramset_union [in Typing]
paramSubst_in_fieldTermList [in Substitutions]
paramSubst_in_paramTermList [in Substitutions]
paramSubst_in_path [in Substitutions]
paramSubst_in_term [in Substitutions]
paramSubst_in_type [in Substitutions]
params_evaluated [in Proofs_Progress]
params_of_paramTermList [in Typing]
params_of_paramTypeList [in Proofs_SubstitutionLemmas2]
params_of_paramValueList [in Proofs_SubstitutionLemmas2]
ParamTypeList [in Typing]
paramTypeList_to_paramList [in Proofs_Miscellaneous]
ParamValueList [in Subclassing]
paramValueList_to_paramList [in Proofs_Miscellaneous]
paramValueList_to_ParamTermList [in Substitutions]
param_in_path [in Typing]
param_in_term [in Typing]
param_in_type [in Typing]
path_is_var_closed [in DeBruijn]
path_is_var_closed' [in DeBruijn]
path_to_term [in Subclassing]
polySubst_in_termValue_prop1 [in Substitutions]
polySubst_in_termValue_prop2 [in Substitutions]
R
Red_term_star [in Proofs_Soundness]
rootEnv [in Typing]
S
Sym [in Calculus]
symbol_of_type [in TypeOrdering]
symRel_is_well_founded [in WellFormedness]
T
term_evaluated [in Subclassing]
term_is_var_closed [in DeBruijn]
term_is_var_closed' [in DeBruijn]
thisSubst_in_fieldTermList [in Substitutions]
thisSubst_in_paramTermList [in Substitutions]
thisSubst_in_paramTypeList [in Proofs_SubstitutionLemmas]
thisSubst_in_path [in Substitutions]
thisSubst_in_term [in Substitutions]
thisSubst_in_type [in Substitutions]
thisSubst_in_typeList [in Proofs_SubstitutionLemmas]
this_in_path [in Typing]
this_in_type [in Typing]
typeDefs_are_well_formed [in WellFormedness]
TypeList [in Typing]
typeRel [in TypeOrdering]
typeRelMul [in Proofs_TypeOrdering]
typeVals_are_well_formed [in WellFormedness]
type_is_closed [in Typing]
type_is_var_closed [in DeBruijn]
type_is_var_closed' [in DeBruijn]
V
ValueList [in Subclassing]
Value_eqdec' [in Proofs_Miscellaneous]
value_to_term [in Subclassing]
VarSet [in DeBruijn]
varset_add [in DeBruijn]
varset_In [in DeBruijn]
varset_union [in DeBruijn]
varSubst_in_fieldTermList [in Substitutions]
varSubst_in_paramTermList [in Substitutions]
varSubst_in_path [in Substitutions]
varSubst_in_term [in Substitutions]
varSubst_in_type [in Substitutions]
VarSym [in Calculus]
var_in_path [in DeBruijn]
var_in_term [in DeBruijn]
var_in_type [in DeBruijn]
Module Index
E
ESM [in Proofs_TypeOrdering]
ESM [in Proofs_TypeOrdering]
M
My_DeBruijn [in TypeOrdering]
My_Proofs_AdmissibilityOfTransitivity [in Proofs_Progress]
My_Proofs_DeBruijnSIndices [in Proofs_SubstitutionLemmas]
My_Proofs_Miscellaneous [in Proofs_TypeOrdering]
My_Proofs_Progress [in Proofs_DeBruijnSIndices]
My_Proofs_Subclassing [in Proofs_AdmissibilityOfTransitivity]
My_Proofs_SubjectReduction [in Proofs_Soundness]
My_Proofs_SubstitutionLemmas [in Proofs_SubstitutionLemmas2]
My_Proofs_SubstitutionLemmas2 [in Proofs_SubstitutionLemmas3]
My_Proofs_SubstitutionLemmas3 [in Proofs_SubjectReduction]
My_Proofs_TypeOrdering [in Proofs_Subclassing]
My_Semantics [in WellFormedness]
My_Subclassing [in Substitutions]
My_Substitutions [in DeBruijn]
My_TypeOrdering [in Typing]
My_Typing [in Semantics]
My_WellFormedness [in Proofs_Miscellaneous]
N
NoConstraint [in Typing]
P
Program [in Calculus]
S
SetProgram [in Proofs_TypeOrdering]
SetProgram [in Proofs_SubjectReduction]
SetProgram [in Proofs_SubstitutionLemmas2]
SetProgram [in Proofs_Miscellaneous]
SetProgram [in Semantics]
SetProgram [in Proofs_DeBruijnSIndices]
SetProgram [in TypeOrdering]
SetProgram [in Proofs_SubstitutionLemmas3]
SetProgram [in Proofs_Soundness]
SetProgram [in Proofs_Progress]
SetProgram [in WellFormedness]
SetProgram [in Typing]
SetProgram [in Proofs_AdmissibilityOfTransitivity]
SetProgram [in Proofs_Subclassing]
SetProgram [in Subclassing]
SetProgram [in Substitutions]
SetProgram [in Proofs_SubstitutionLemmas]
SetProgram [in DeBruijn]
Sid [in Proofs_TypeOrdering]
StructuredTypingRelations [in Typing]
SymbolConstraint [in Typing]
T
TransitivityConstraint [in Typing]
Type_Eqset [in Proofs_TypeOrdering]
Type_Eqset_dec [in Proofs_TypeOrdering]
Type_Multiset [in Proofs_TypeOrdering]
Type_MultisetOrder [in Proofs_TypeOrdering]
TypingRelations [in Typing]
Library Index
C
Calculus
D
DeBruijn
M
MatchCompNat
P
Proofs_AdmissibilityOfTransitivity
Proofs_DeBruijnSIndices
Proofs_Miscellaneous
Proofs_Progress
Proofs_Soundness
Proofs_Subclassing
Proofs_SubjectReduction
Proofs_SubstitutionLemmas
Proofs_SubstitutionLemmas2
Proofs_SubstitutionLemmas3
Proofs_TypeOrdering
S
Semantics
Subclassing
Substitutions
T
TypeOrdering
Typing
U
Util
W
WellFormedness
WellFoundation
| 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 |
_ |
(769 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 |
_ |
(27 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 |
_ |
(303 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 |
_ |
(94 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 |
_ |
(40 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 |
_ |
(235 entries) |
| Module Index |
A |
B |
C |
D |
E |
F |
G |
H |
I |
J |
K |
L |
M |
N |
O |
P |
Q |
R |
S |
T |
U |
V |
W |
X |
Y |
Z |
_ |
(48 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 |
_ |
(22 entries) |
This page has been generated by coqdoc