Module

# Data.HeytingAlgebra

Package
purescript-prelude
Repository
purescript/purescript-prelude

### #HeytingAlgebraSource

``class HeytingAlgebra a  where``

The `HeytingAlgebra` type class represents types that are bounded lattices with an implication operator such that the following laws hold:

• 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`

#### Members

• `ff :: a`
• `tt :: a`
• `implies :: a -> a -> a`
• `conj :: a -> a -> a`
• `disj :: a -> a -> a`
• `not :: a -> a`

#### Instances

• `HeytingAlgebra Boolean`
• `HeytingAlgebra Unit`
• `(HeytingAlgebra b) => HeytingAlgebra (a -> b)`

### #(&&)Source

Operator alias for Data.HeytingAlgebra.conj (right-associative / precedence 3)

### #(||)Source

Operator alias for Data.HeytingAlgebra.disj (right-associative / precedence 2)