Module Qcert.TypeSystem.ForeignType

Require Import EquivDec.
Require Import Lattice.

Section ForeignType.
  
  Class foreign_type : Type
    := mk_foreign_type {
           foreign_type_type : Set
           ; foreign_type_dec :> EqDec foreign_type_type eq
           ; foreign_type_lattice :> Lattice foreign_type_type eq
           ; foreign_type_sub (a b : foreign_type_type) : Prop
           ; foreign_type_sub_dec (a b : foreign_type_type) :
               { foreign_type_sub a b} + {~ foreign_type_sub a b}
           ; foreign_type_sub_pre :> PreOrder foreign_type_sub
           ; foreign_type_sub_part :> PartialOrder eq foreign_type_sub
           ; foreign_type_olattice :> OLattice eq foreign_type_sub
      }.
  
End ForeignType.