Module

# Data.BooleanAlgebra

Package
purescript-prelude
Repository
purescript/purescript-prelude

### #BooleanAlgebraSource

``class (HeytingAlgebra a) <= BooleanAlgebra a ``

The `BooleanAlgebra` type class represents types that behave like boolean values.

Instances should satisfy the following laws in addition to the `HeytingAlgebra` law:

• Excluded middle:
• `a || not a = tt`

#### Instances

• `BooleanAlgebra Boolean`
• `BooleanAlgebra Unit`
• `(BooleanAlgebra b) => BooleanAlgebra (a -> b)`
• `(RowToList row list, BooleanAlgebraRecord list row row) => BooleanAlgebra { | row }`

### #BooleanAlgebraRecordSource

``class (HeytingAlgebraRecord rowlist row subrow) <= BooleanAlgebraRecord rowlist row subrow | rowlist -> subrow``

A class for records where all fields have `BooleanAlgebra` instances, used to implement the `BooleanAlgebra` instance for records.

#### Instances

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

## Re-exports from Data.HeytingAlgebra

### #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)`
• `(RowToList row list, HeytingAlgebraRecord list row row) => HeytingAlgebra { | row }`

### #HeytingAlgebraRecordSource

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

A class for records where all fields have `HeytingAlgebra` instances, used to implement the `HeytingAlgebra` instance for records.

#### Instances

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

### #(||)Source

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

### #(&&)Source

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