gcounter.idr

module Main
 
import Prelude.Algebra

record GCounter : Type where
  MkGCounter : (value : Int) -> GCounter

gcjoin : GCounter -> GCounter -> GCounter
gcjoin l r = (MkGCounter ((value l) + (value r)))

gc1 : GCounter
gc1 = (MkGCounter 1)

gc2 : GCounter
gc2 = (MkGCounter 2)

instance JoinSemilattice GCounter where
  join = gcjoin
  
instance VerifiedJoinSemilattice GCounter where
  joinSemilatticeJoinIsAssociative = ?a
  joinSemilatticeJoinIsCommutative = ?c
  joinSemilatticeJoinIsIdempotent  = ?i