Algebra.Heyting.Properties

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

Documentation

data BoundedMeetSemiLatticeLawViolation a

Constructors

BMSLVNonAssociative a a a

BMSLVNonCommutative a a

BMSLVNonIdempotent a

BMSLVNonUnital a

BMSLVMeetOrderViolation a a

Instances

Eq a => Eq (BoundedMeetSemiLatticeLawViolation a)

Defined in Algebra.Heyting.Properties

Methods

(==) :: BoundedMeetSemiLatticeLawViolation a -> BoundedMeetSemiLatticeLawViolation a -> Bool

(/=) :: BoundedMeetSemiLatticeLawViolation a -> BoundedMeetSemiLatticeLawViolation a -> Bool

Ord a => Ord (BoundedMeetSemiLatticeLawViolation a)

Defined in Algebra.Heyting.Properties

Methods

compare :: BoundedMeetSemiLatticeLawViolation a -> BoundedMeetSemiLatticeLawViolation a -> Ordering

(<) :: BoundedMeetSemiLatticeLawViolation a -> BoundedMeetSemiLatticeLawViolation a -> Bool

(<=) :: BoundedMeetSemiLatticeLawViolation a -> BoundedMeetSemiLatticeLawViolation a -> Bool

(>) :: BoundedMeetSemiLatticeLawViolation a -> BoundedMeetSemiLatticeLawViolation a -> Bool

(>=) :: BoundedMeetSemiLatticeLawViolation a -> BoundedMeetSemiLatticeLawViolation a -> Bool

max :: BoundedMeetSemiLatticeLawViolation a -> BoundedMeetSemiLatticeLawViolation a -> BoundedMeetSemiLatticeLawViolation a

min :: BoundedMeetSemiLatticeLawViolation a -> BoundedMeetSemiLatticeLawViolation a -> BoundedMeetSemiLatticeLawViolation a

Show a => Show (BoundedMeetSemiLatticeLawViolation a)

Defined in Algebra.Heyting.Properties

Methods

showsPrec :: Int -> BoundedMeetSemiLatticeLawViolation a -> ShowS

show :: BoundedMeetSemiLatticeLawViolation a -> String

showList :: [BoundedMeetSemiLatticeLawViolation a] -> ShowS

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

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

Verifies bounded meet semilattice laws.

data BoundedJoinSemiLatticeLawViolation a

Constructors

BJSLVNonAssociative a a a

BJSLVNonCommutative a a

BJSLVNonIdempotent a

BJSLVNonUnital a

BJSLVJoinOrderViolation a a

Instances

Eq a => Eq (BoundedJoinSemiLatticeLawViolation a)

Defined in Algebra.Heyting.Properties

Methods

(==) :: BoundedJoinSemiLatticeLawViolation a -> BoundedJoinSemiLatticeLawViolation a -> Bool

(/=) :: BoundedJoinSemiLatticeLawViolation a -> BoundedJoinSemiLatticeLawViolation a -> Bool

Ord a => Ord (BoundedJoinSemiLatticeLawViolation a)

Defined in Algebra.Heyting.Properties

Methods

compare :: BoundedJoinSemiLatticeLawViolation a -> BoundedJoinSemiLatticeLawViolation a -> Ordering

(<) :: BoundedJoinSemiLatticeLawViolation a -> BoundedJoinSemiLatticeLawViolation a -> Bool

(<=) :: BoundedJoinSemiLatticeLawViolation a -> BoundedJoinSemiLatticeLawViolation a -> Bool

(>) :: BoundedJoinSemiLatticeLawViolation a -> BoundedJoinSemiLatticeLawViolation a -> Bool

(>=) :: BoundedJoinSemiLatticeLawViolation a -> BoundedJoinSemiLatticeLawViolation a -> Bool

max :: BoundedJoinSemiLatticeLawViolation a -> BoundedJoinSemiLatticeLawViolation a -> BoundedJoinSemiLatticeLawViolation a

min :: BoundedJoinSemiLatticeLawViolation a -> BoundedJoinSemiLatticeLawViolation a -> BoundedJoinSemiLatticeLawViolation a

Show a => Show (BoundedJoinSemiLatticeLawViolation a)

Defined in Algebra.Heyting.Properties

Methods

showsPrec :: Int -> BoundedJoinSemiLatticeLawViolation a -> ShowS

show :: BoundedJoinSemiLatticeLawViolation a -> String

showList :: [BoundedJoinSemiLatticeLawViolation a] -> ShowS

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

Verifies bounded join semilattice laws.

data DistributiveLatticeLawViolation a

Constructors

DLLVJoinOverMeetViolation a a a

DLLVMeetOverJoinViolation a a a

Instances

Eq a => Eq (DistributiveLatticeLawViolation a)

Defined in Algebra.Heyting.Properties

Methods

(==) :: DistributiveLatticeLawViolation a -> DistributiveLatticeLawViolation a -> Bool

(/=) :: DistributiveLatticeLawViolation a -> DistributiveLatticeLawViolation a -> Bool

Ord a => Ord (DistributiveLatticeLawViolation a)

Defined in Algebra.Heyting.Properties

Methods

compare :: DistributiveLatticeLawViolation a -> DistributiveLatticeLawViolation a -> Ordering

(<) :: DistributiveLatticeLawViolation a -> DistributiveLatticeLawViolation a -> Bool

(<=) :: DistributiveLatticeLawViolation a -> DistributiveLatticeLawViolation a -> Bool

(>) :: DistributiveLatticeLawViolation a -> DistributiveLatticeLawViolation a -> Bool

(>=) :: DistributiveLatticeLawViolation a -> DistributiveLatticeLawViolation a -> Bool

max :: DistributiveLatticeLawViolation a -> DistributiveLatticeLawViolation a -> DistributiveLatticeLawViolation a

min :: DistributiveLatticeLawViolation a -> DistributiveLatticeLawViolation a -> DistributiveLatticeLawViolation a

Show a => Show (DistributiveLatticeLawViolation a)

Defined in Algebra.Heyting.Properties

Methods

showsPrec :: Int -> DistributiveLatticeLawViolation a -> ShowS

show :: DistributiveLatticeLawViolation a -> String

showList :: [DistributiveLatticeLawViolation a] -> ShowS

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

Distributivity laws for a lattice.

data HeytingAlgebraLawViolation a

Constructors

HAVImplication1 a a a

HAVImplication2 a a a

HAVNot a a

HAVNotAndMeet a a

HAVNotAndJoin a a

HAVImplicationAndOrd a a

HAVDistributiveLatticeLawViolation (DistributiveLatticeLawViolation a)

HAVBoundedJoinSemilatticeLawViolation (BoundedJoinSemiLatticeLawViolation a)

HAVBoundedMeetSemilatticeLawViolation (BoundedMeetSemiLatticeLawViolation a)

Instances

Eq a => Eq (HeytingAlgebraLawViolation a)

Defined in Algebra.Heyting.Properties

Methods

(==) :: HeytingAlgebraLawViolation a -> HeytingAlgebraLawViolation a -> Bool

(/=) :: HeytingAlgebraLawViolation a -> HeytingAlgebraLawViolation a -> Bool

Ord a => Ord (HeytingAlgebraLawViolation a)

Defined in Algebra.Heyting.Properties

Methods

compare :: HeytingAlgebraLawViolation a -> HeytingAlgebraLawViolation a -> Ordering

(<) :: HeytingAlgebraLawViolation a -> HeytingAlgebraLawViolation a -> Bool

(<=) :: HeytingAlgebraLawViolation a -> HeytingAlgebraLawViolation a -> Bool

(>) :: HeytingAlgebraLawViolation a -> HeytingAlgebraLawViolation a -> Bool

(>=) :: HeytingAlgebraLawViolation a -> HeytingAlgebraLawViolation a -> Bool

max :: HeytingAlgebraLawViolation a -> HeytingAlgebraLawViolation a -> HeytingAlgebraLawViolation a

min :: HeytingAlgebraLawViolation a -> HeytingAlgebraLawViolation a -> HeytingAlgebraLawViolation a

Show a => Show (HeytingAlgebraLawViolation a)

Defined in Algebra.Heyting.Properties

Methods

showsPrec :: Int -> HeytingAlgebraLawViolation a -> ShowS

show :: HeytingAlgebraLawViolation a -> String

showList :: [HeytingAlgebraLawViolation a] -> ShowS

prop_implies :: (Heyting a, Ord a, Eq a, Show a) => a -> a -> a -> CounterExample (HeytingAlgebraLawViolation a)

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 :: (Heyting a, Ord a, Eq a, Show a) => a -> a -> a -> CounterExample (HeytingAlgebraLawViolation a)

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

• bounded lattice laws

• prop_implies