Module

Data.BooleanAlgebra

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:

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

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

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

class HeytingAlgebraRecord rowlist row subrow | rowlist -> subrow

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

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

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