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)`
• `HeytingAlgebra (Proxy a)`
• `HeytingAlgebra (Proxy2 a)`
• `HeytingAlgebra (Proxy3 a)`
• `(RowToList row list, HeytingAlgebraRecord list row row) => HeytingAlgebra (Record row)`

### #(&&)Source

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

### #(||)Source

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

### #HeytingAlgebraRecordSource

``class HeytingAlgebraRecord rowlist row subrow | rowlist -> subrow where``

#### Members

• `ffRecord :: forall rlproxy rproxy. rlproxy rowlist -> rproxy row -> Record subrow`
• `ttRecord :: forall rlproxy rproxy. rlproxy rowlist -> rproxy row -> Record subrow`
• `impliesRecord :: forall rlproxy. rlproxy rowlist -> Record row -> Record row -> Record subrow`
• `disjRecord :: forall rlproxy. rlproxy rowlist -> Record row -> Record row -> Record subrow`
• `conjRecord :: forall rlproxy. rlproxy rowlist -> Record row -> Record row -> Record subrow`
• `notRecord :: forall rlproxy. rlproxy rowlist -> Record row -> Record subrow`

#### Instances

• `HeytingAlgebraRecord Nil row ()`
• `(IsSymbol key, Cons key focus subrowTail subrow, HeytingAlgebraRecord rowlistTail row subrowTail, HeytingAlgebra focus) => HeytingAlgebraRecord (Cons key focus rowlistTail) row subrow`