Module RTypeLattice

Require Import String.
Require Import List.
Require Import Bool.
Require Import RelationClasses.
Require Import EquivDec.

Require Import Utils.
Require Import ForeignType.
Require Import RType.
Require Import RSubtypeProp.
Require Import RTypeMeetJoin.
Require Import RTypeMeetJoin RConsistentSubtype.
Require Import BrandRelation.
Require Import Lattice.

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.