Qcert.Basic.TypeSystem.ForeignType

Section TForeign.


  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 TForeign.