Bounded package:lattices

class Lattice a => BoundedJoinSemiLattice a

A join-semilattice with an identity element bottom for \/. Laws

x \/ bottom ≡ x

Corollary

x /\ bottom
≡⟨ identity ⟩
(x /\ bottom) \/ bottom
≡⟨ absorption ⟩
bottom

type BoundedLattice a = (BoundedMeetSemiLattice a, BoundedJoinSemiLattice a)

class Lattice a => BoundedMeetSemiLattice a

A meet-semilattice with an identity element top for /\. Laws

x /\ top ≡ x

Corollary

x \/ top
≡⟨ identity ⟩
(x \/ top) /\ top
≡⟨ absorption ⟩
top

data FBoundedLattice a