Qcert.Basic.TypeSystem.RTypeLattice

Section RTypeLattice.

  Context {ftype:foreign_type}.
  Context {br:brand_relation}.

  Global Instance rtype_lattice : Lattice rtype eq
    := { meet:=rtype_meet;
         join:=rtype_join;
         meet_commutative := rtype_meet_commutative;
         meet_associative := rtype_meet_associative;
         meet_idempotent := rtype_meet_idempotent;
         join_commutative := rtype_join_commutative;
         join_associative := rtype_join_associative;
         join_idempotent := rtype_join_idempotent;
         meet_absorptive := rtype_meet_absorptive;
         join_absorptive := rtype_join_absorptive
       }.

  Global Instance rtype_olattice :
    OLattice eq subtype
    := { consistent_meet := consistent_rtype_meet }.



End RTypeLattice.