Library TypeOrdering

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.

Index
This page has been generated by coqdoc