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

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

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

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

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)