Module
Data.HeytingAlgebra
#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
Members
Instances
HeytingAlgebra Boolean
HeytingAlgebra Unit
(HeytingAlgebra b) => HeytingAlgebra (a -> b)
(RowToList row list, HeytingAlgebraRecord list row row) => HeytingAlgebra { | row }
#(&&)
Operator alias for Data.HeytingAlgebra.conj (right-associative / precedence 3)
#(||)
Operator alias for Data.HeytingAlgebra.disj (right-associative / precedence 2)
#HeytingAlgebraRecord
class HeytingAlgebraRecord rowlist row subrow | rowlist -> subrow where
A class for records where all fields have HeytingAlgebra
instances, used
to implement the HeytingAlgebra
instance for records.
Members
ffRecord :: RLProxy rowlist -> RProxy row -> { | subrow }
ttRecord :: RLProxy rowlist -> RProxy row -> { | subrow }
impliesRecord :: RLProxy rowlist -> { | row } -> { | row } -> { | subrow }
disjRecord :: RLProxy rowlist -> { | row } -> { | row } -> { | subrow }
conjRecord :: RLProxy rowlist -> { | row } -> { | row } -> { | subrow }
notRecord :: RLProxy rowlist -> { | row } -> { | 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
Modules
- Control.Applicative
- Control.Apply
- Control.Bind
- Control.Category
- Control.Monad
- Control.Semigroupoid
- Data.Boolean
- Data.BooleanAlgebra
- Data.Bounded
- Data.CommutativeRing
- Data.DivisionRing
- Data.Eq
- Data.EuclideanRing
- Data.Field
- Data.Function
- Data.Functor
- Data.HeytingAlgebra
- Data.Monoid
- Data.Monoid.Additive
- Data.Monoid.Conj
- Data.Monoid.Disj
- Data.Monoid.Dual
- Data.Monoid.Endo
- Data.Monoid.Multiplicative
- Data.NaturalTransformation
- Data.Ord
- Data.Ord.Unsafe
- Data.Ordering
- Data.Ring
- Data.Semigroup
- Data.Semigroup.First
- Data.Semigroup.Last
- Data.Semiring
- Data.Show
- Data.Symbol
- Data.Unit
- Data.Void
- Effect
- Effect.Class
- Effect.Class.Console
- Effect.Console
- Effect.Uncurried
- Effect.Unsafe
- Main
- PSCI.Support
- Prelude
- Prim
- Prim.Ordering
- Prim.Row
- Prim.RowList
- Prim.Symbol
- Prim.TypeError
- Record.Unsafe
- Type.Data.Boolean
- Type.Data.Ordering
- Type.Data.Row
- Type.Data.RowList
- Type.Data.Symbol
- Type.Equality
- Type.Prelude
- Type.Proxy
- Type.Row
- Type.Row.Homogeneous