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

Relation: well-founded relation on types
Definition typeRel (T: type) (U: type): Prop :=
  symRel (symbol_of_type T) (symbol_of_type U)

End SetProgram.

This page has been generated by coqdoc