Definition of Type Ordering |
Require Import Calculus.
Module SetProgram(My_Program: Program).
Import My_Program.
Require DeBruijn.
Module My_DeBruijn := DeBruijn.SetProgram(My_Program).
Import My_DeBruijn.
Import My_Substitutions.
Import My_Subclassing.
| Function: return the main symbol of a type |
Definition symbol_of_type (T: type): Sym :=
match T with
| (type_class C) => inl _ C
| (type_virtual p L) => inr _ L
end
.
| Relation: well-founded relation on types |
Definition typeRel (T: type) (U: type): Prop :=
symRel (symbol_of_type T) (symbol_of_type U)
.
End SetProgram.