DistributiveLattice?

[clayrat]

I think there's a requirement for Heyting algebras to be both distributive and bounded lattices, so it would be nice to add

interface Lattice a => VerifiedDistributiveLattice a where
  meetDistributesOverJoin : (x, y, z : a) -> x `meet` (y `join` z) = (x `meet` y) `join` (x `meet` z).

(the dual follows from this, which should probably be also added)
So that

interface (VerifiedBoundedJoinSemilattice a, VerifiedBoundedMeetSemilattice a, VerifiedDistributiveLattice a, HeytingAlgebra a) => VerifiedHeytingAlgebra a where

[Risto-Stevcev]

Thanks for the heads up, I wasn't aware of that one. I added the constraint 🙂