Test.QuickCheck.Laws.Data.HeytingAlgebra

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 :: forall a. HeytingAlgebra a => Eq a => Gen a -> Effect Unit