Module

Test.QuickCheck.Laws.Data.HeytingAlgebra

#checkHeytingAlgebra 

checkHeytingAlgebra :: forall a. Arbitrary a => HeytingAlgebra a => Eq a => Proxy a -> Effect Unit
  • Associativity:
    • a || (b || c) = (a || b) || c
    • a && (b && c) = (a && b) && c
  • Commutativity:
    • a || b = b || a
    • a && b = b && a
  • Absorption:
    • a || (a && b) = a
    • a && (a || b) = a
  • Idempotent:
    • a || a = a
    • a && a = a
  • Identity:
    • a || ff = a
    • a && tt = a
  • Implication:
    • a `implies` a = tt
    • a && (a `implies` b) = a && b
    • b && (a `implies` b) = b
    • a `implies` (b && c) = (a `implies` b) && (a `implies` c)
  • Complemented:
    • not a = a `implies` ff

#checkHeytingAlgebraGen 

checkHeytingAlgebraGen :: forall a. HeytingAlgebra a => Eq a => Gen a -> Effect Unit

Modules