heyting-algebras-0.0.2.0: Heyting and Boolean algebras

Safe HaskellSafe
LanguageHaskell2010

Algebra.Heyting.Properties

Description

Properties of Heyting algebras; useful for testing lawfulness of instances.

Synopsis

Documentation

data BoundedMeetSemiLatticeLawViolation a Source #

withArgs :: Show a => String -> [a] -> String Source #

prop_BoundedMeetSemiLattice :: (BoundedMeetSemiLattice a, Ord a, Eq a, Show a) => a -> a -> a -> CounterExample (BoundedMeetSemiLatticeLawViolation a) Source #

Verifies bounded meet semilattice laws.

data BoundedJoinSemiLatticeLawViolation a Source #

prop_BoundedJoinSemiLattice :: (BoundedJoinSemiLattice a, Ord a, Eq a, Show a) => a -> a -> a -> CounterExample (BoundedJoinSemiLatticeLawViolation a) Source #

Verifies bounded join semilattice laws.

data DistributiveLatticeLawViolation a Source #

prop_DistributiveLattice :: (Lattice a, Ord a, Eq a, Show a) => a -> a -> a -> CounterExample (DistributiveLatticeLawViolation a) Source #

Distributivity laws for a lattice.

data HeytingAlgebraLawViolation a Source #

prop_implies :: (HeytingAlgebra a, Ord a, Eq a, Show a) => a -> a -> a -> CounterExample (HeytingAlgebraLawViolation a) Source #

Verifies the Heyting algebra law for ==>: for all a: _ / a is left adjoint to a ==> and some other properties that are a consequence of that.

prop_HeytingAlgebra :: (HeytingAlgebra a, Ord a, Eq a, Show a) => a -> a -> a -> CounterExample (HeytingAlgebraLawViolation a) Source #

Useful for testing valid instances of HeytingAlgebra type class. It validates: