{-# LANGUAGE CPP #-}
{-# LANGUAGE DeriveDataTypeable #-}
{-# LANGUAGE DeriveGeneric #-}
{-# LANGUAGE GeneralizedNewtypeDeriving #-}
module Algebra.Boolean
  ( BooleanAlgebra
  , (==>)
  , neg
    -- * Adjunction between Boolean and Heyting algebras
  , Boolean
  , runBooleanAlgebra
  , boolean
  ) where

import           Control.Applicative    (Const (..))
import           Data.Data              (Data, Typeable)
import           Data.Functor.Identity  (Identity (..))
import           Data.Proxy             (Proxy (..))
import           Data.Semigroup         ( All (..)
                                        , Any (..)
                                        , Endo (..)
                                        )
import           Data.Tagged            (Tagged (..))
import           GHC.Generics           (Generic)

import           Algebra.Heyting
import           Algebra.Lattice        ( Lattice
                                        , BoundedJoinSemiLattice
                                        , BoundedMeetSemiLattice
                                        )

class Heyting a => Boolean a

instance Boolean Bool

instance Boolean All

instance Boolean Any

instance Boolean ()

instance Boolean (Proxy a)

instance Boolean a => Boolean (Tagged t a)

instance Boolean b => Boolean (a -> b)

#if MIN_VERSION_base(4,8,0)
instance Boolean a => Boolean (Identity a)
#endif

instance Boolean a => Boolean (Const a b)

instance Boolean a => Boolean (Endo a)

-- | Every Heyting algebra contains a Boolean algebra. @'toBoolean'@ maps onto
-- it; moreover it is a monad (Heyting algebra is a category as every poset is)
-- which preserves finite infima.
--
toBoolean :: Heyting a => a -> a
toBoolean :: a -> a
toBoolean = a -> a
forall a. Heyting a => a -> a
neg (a -> a) -> (a -> a) -> a -> a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> a
forall a. Heyting a => a -> a
neg

-- |
-- @'Boolean'@ is the left adjoint functor from the category of Heyting algebras
-- to the category of Boolean algebras; its right adjoint is the inclusion.
newtype BooleanAlgebra a = BooleanAlgebra
    { BooleanAlgebra a -> a
runBooleanAlgebra :: a -- ^ extract value from @'Boolean'@
    }
  deriving
    ( Lattice (BooleanAlgebra a)
BooleanAlgebra a
Lattice (BooleanAlgebra a)
-> BooleanAlgebra a -> BoundedJoinSemiLattice (BooleanAlgebra a)
forall a. Lattice a -> a -> BoundedJoinSemiLattice a
forall a. BoundedJoinSemiLattice a => Lattice (BooleanAlgebra a)
forall a. BoundedJoinSemiLattice a => BooleanAlgebra a
bottom :: BooleanAlgebra a
$cbottom :: forall a. BoundedJoinSemiLattice a => BooleanAlgebra a
$cp1BoundedJoinSemiLattice :: forall a. BoundedJoinSemiLattice a => Lattice (BooleanAlgebra a)
BoundedJoinSemiLattice
    , Lattice (BooleanAlgebra a)
BooleanAlgebra a
Lattice (BooleanAlgebra a)
-> BooleanAlgebra a -> BoundedMeetSemiLattice (BooleanAlgebra a)
forall a. Lattice a -> a -> BoundedMeetSemiLattice a
forall a. BoundedMeetSemiLattice a => Lattice (BooleanAlgebra a)
forall a. BoundedMeetSemiLattice a => BooleanAlgebra a
top :: BooleanAlgebra a
$ctop :: forall a. BoundedMeetSemiLattice a => BooleanAlgebra a
$cp1BoundedMeetSemiLattice :: forall a. BoundedMeetSemiLattice a => Lattice (BooleanAlgebra a)
BoundedMeetSemiLattice
    , BooleanAlgebra a -> BooleanAlgebra a -> BooleanAlgebra a
(BooleanAlgebra a -> BooleanAlgebra a -> BooleanAlgebra a)
-> (BooleanAlgebra a -> BooleanAlgebra a -> BooleanAlgebra a)
-> Lattice (BooleanAlgebra a)
forall a.
Lattice a =>
BooleanAlgebra a -> BooleanAlgebra a -> BooleanAlgebra a
forall a. (a -> a -> a) -> (a -> a -> a) -> Lattice a
/\ :: BooleanAlgebra a -> BooleanAlgebra a -> BooleanAlgebra a
$c/\ :: forall a.
Lattice a =>
BooleanAlgebra a -> BooleanAlgebra a -> BooleanAlgebra a
\/ :: BooleanAlgebra a -> BooleanAlgebra a -> BooleanAlgebra a
$c\/ :: forall a.
Lattice a =>
BooleanAlgebra a -> BooleanAlgebra a -> BooleanAlgebra a
Lattice
    , BoundedLattice (BooleanAlgebra a)
BoundedLattice (BooleanAlgebra a)
-> (BooleanAlgebra a -> BooleanAlgebra a -> BooleanAlgebra a)
-> (BooleanAlgebra a -> BooleanAlgebra a)
-> (BooleanAlgebra a -> BooleanAlgebra a -> BooleanAlgebra a)
-> Heyting (BooleanAlgebra a)
BooleanAlgebra a -> BooleanAlgebra a
BooleanAlgebra a -> BooleanAlgebra a -> BooleanAlgebra a
forall a.
BoundedLattice a
-> (a -> a -> a) -> (a -> a) -> (a -> a -> a) -> Heyting a
forall a. Heyting a => BoundedLattice (BooleanAlgebra a)
forall a. Heyting a => BooleanAlgebra a -> BooleanAlgebra a
forall a.
Heyting a =>
BooleanAlgebra a -> BooleanAlgebra a -> BooleanAlgebra a
<=> :: BooleanAlgebra a -> BooleanAlgebra a -> BooleanAlgebra a
$c<=> :: forall a.
Heyting a =>
BooleanAlgebra a -> BooleanAlgebra a -> BooleanAlgebra a
neg :: BooleanAlgebra a -> BooleanAlgebra a
$cneg :: forall a. Heyting a => BooleanAlgebra a -> BooleanAlgebra a
==> :: BooleanAlgebra a -> BooleanAlgebra a -> BooleanAlgebra a
$c==> :: forall a.
Heyting a =>
BooleanAlgebra a -> BooleanAlgebra a -> BooleanAlgebra a
$cp1Heyting :: forall a. Heyting a => BoundedLattice (BooleanAlgebra a)
Heyting
    , BooleanAlgebra a -> BooleanAlgebra a -> Bool
(BooleanAlgebra a -> BooleanAlgebra a -> Bool)
-> (BooleanAlgebra a -> BooleanAlgebra a -> Bool)
-> Eq (BooleanAlgebra a)
forall a. Eq a => BooleanAlgebra a -> BooleanAlgebra a -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: BooleanAlgebra a -> BooleanAlgebra a -> Bool
$c/= :: forall a. Eq a => BooleanAlgebra a -> BooleanAlgebra a -> Bool
== :: BooleanAlgebra a -> BooleanAlgebra a -> Bool
$c== :: forall a. Eq a => BooleanAlgebra a -> BooleanAlgebra a -> Bool
Eq, Eq (BooleanAlgebra a)
Eq (BooleanAlgebra a)
-> (BooleanAlgebra a -> BooleanAlgebra a -> Ordering)
-> (BooleanAlgebra a -> BooleanAlgebra a -> Bool)
-> (BooleanAlgebra a -> BooleanAlgebra a -> Bool)
-> (BooleanAlgebra a -> BooleanAlgebra a -> Bool)
-> (BooleanAlgebra a -> BooleanAlgebra a -> Bool)
-> (BooleanAlgebra a -> BooleanAlgebra a -> BooleanAlgebra a)
-> (BooleanAlgebra a -> BooleanAlgebra a -> BooleanAlgebra a)
-> Ord (BooleanAlgebra a)
BooleanAlgebra a -> BooleanAlgebra a -> Bool
BooleanAlgebra a -> BooleanAlgebra a -> Ordering
BooleanAlgebra a -> BooleanAlgebra a -> BooleanAlgebra a
forall a.
Eq a
-> (a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
forall a. Ord a => Eq (BooleanAlgebra a)
forall a. Ord a => BooleanAlgebra a -> BooleanAlgebra a -> Bool
forall a. Ord a => BooleanAlgebra a -> BooleanAlgebra a -> Ordering
forall a.
Ord a =>
BooleanAlgebra a -> BooleanAlgebra a -> BooleanAlgebra a
min :: BooleanAlgebra a -> BooleanAlgebra a -> BooleanAlgebra a
$cmin :: forall a.
Ord a =>
BooleanAlgebra a -> BooleanAlgebra a -> BooleanAlgebra a
max :: BooleanAlgebra a -> BooleanAlgebra a -> BooleanAlgebra a
$cmax :: forall a.
Ord a =>
BooleanAlgebra a -> BooleanAlgebra a -> BooleanAlgebra a
>= :: BooleanAlgebra a -> BooleanAlgebra a -> Bool
$c>= :: forall a. Ord a => BooleanAlgebra a -> BooleanAlgebra a -> Bool
> :: BooleanAlgebra a -> BooleanAlgebra a -> Bool
$c> :: forall a. Ord a => BooleanAlgebra a -> BooleanAlgebra a -> Bool
<= :: BooleanAlgebra a -> BooleanAlgebra a -> Bool
$c<= :: forall a. Ord a => BooleanAlgebra a -> BooleanAlgebra a -> Bool
< :: BooleanAlgebra a -> BooleanAlgebra a -> Bool
$c< :: forall a. Ord a => BooleanAlgebra a -> BooleanAlgebra a -> Bool
compare :: BooleanAlgebra a -> BooleanAlgebra a -> Ordering
$ccompare :: forall a. Ord a => BooleanAlgebra a -> BooleanAlgebra a -> Ordering
$cp1Ord :: forall a. Ord a => Eq (BooleanAlgebra a)
Ord, ReadPrec [BooleanAlgebra a]
ReadPrec (BooleanAlgebra a)
Int -> ReadS (BooleanAlgebra a)
ReadS [BooleanAlgebra a]
(Int -> ReadS (BooleanAlgebra a))
-> ReadS [BooleanAlgebra a]
-> ReadPrec (BooleanAlgebra a)
-> ReadPrec [BooleanAlgebra a]
-> Read (BooleanAlgebra a)
forall a. Read a => ReadPrec [BooleanAlgebra a]
forall a. Read a => ReadPrec (BooleanAlgebra a)
forall a. Read a => Int -> ReadS (BooleanAlgebra a)
forall a. Read a => ReadS [BooleanAlgebra a]
forall a.
(Int -> ReadS a)
-> ReadS [a] -> ReadPrec a -> ReadPrec [a] -> Read a
readListPrec :: ReadPrec [BooleanAlgebra a]
$creadListPrec :: forall a. Read a => ReadPrec [BooleanAlgebra a]
readPrec :: ReadPrec (BooleanAlgebra a)
$creadPrec :: forall a. Read a => ReadPrec (BooleanAlgebra a)
readList :: ReadS [BooleanAlgebra a]
$creadList :: forall a. Read a => ReadS [BooleanAlgebra a]
readsPrec :: Int -> ReadS (BooleanAlgebra a)
$creadsPrec :: forall a. Read a => Int -> ReadS (BooleanAlgebra a)
Read, Int -> BooleanAlgebra a -> ShowS
[BooleanAlgebra a] -> ShowS
BooleanAlgebra a -> String
(Int -> BooleanAlgebra a -> ShowS)
-> (BooleanAlgebra a -> String)
-> ([BooleanAlgebra a] -> ShowS)
-> Show (BooleanAlgebra a)
forall a. Show a => Int -> BooleanAlgebra a -> ShowS
forall a. Show a => [BooleanAlgebra a] -> ShowS
forall a. Show a => BooleanAlgebra a -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [BooleanAlgebra a] -> ShowS
$cshowList :: forall a. Show a => [BooleanAlgebra a] -> ShowS
show :: BooleanAlgebra a -> String
$cshow :: forall a. Show a => BooleanAlgebra a -> String
showsPrec :: Int -> BooleanAlgebra a -> ShowS
$cshowsPrec :: forall a. Show a => Int -> BooleanAlgebra a -> ShowS
Show, BooleanAlgebra a
BooleanAlgebra a -> BooleanAlgebra a -> Bounded (BooleanAlgebra a)
forall a. a -> a -> Bounded a
forall a. Bounded a => BooleanAlgebra a
maxBound :: BooleanAlgebra a
$cmaxBound :: forall a. Bounded a => BooleanAlgebra a
minBound :: BooleanAlgebra a
$cminBound :: forall a. Bounded a => BooleanAlgebra a
Bounded, Typeable, Typeable (BooleanAlgebra a)
DataType
Constr
Typeable (BooleanAlgebra a)
-> (forall (c :: * -> *).
    (forall d b. Data d => c (d -> b) -> d -> c b)
    -> (forall g. g -> c g)
    -> BooleanAlgebra a
    -> c (BooleanAlgebra a))
-> (forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c (BooleanAlgebra a))
-> (BooleanAlgebra a -> Constr)
-> (BooleanAlgebra a -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c (BooleanAlgebra a)))
-> (forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e))
    -> Maybe (c (BooleanAlgebra a)))
-> ((forall b. Data b => b -> b)
    -> BooleanAlgebra a -> BooleanAlgebra a)
-> (forall r r'.
    (r -> r' -> r)
    -> r -> (forall d. Data d => d -> r') -> BooleanAlgebra a -> r)
-> (forall r r'.
    (r' -> r -> r)
    -> r -> (forall d. Data d => d -> r') -> BooleanAlgebra a -> r)
-> (forall u.
    (forall d. Data d => d -> u) -> BooleanAlgebra a -> [u])
-> (forall u.
    Int -> (forall d. Data d => d -> u) -> BooleanAlgebra a -> u)
-> (forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d)
    -> BooleanAlgebra a -> m (BooleanAlgebra a))
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d)
    -> BooleanAlgebra a -> m (BooleanAlgebra a))
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d)
    -> BooleanAlgebra a -> m (BooleanAlgebra a))
-> Data (BooleanAlgebra a)
BooleanAlgebra a -> DataType
BooleanAlgebra a -> Constr
(forall d. Data d => c (t d)) -> Maybe (c (BooleanAlgebra a))
(forall b. Data b => b -> b)
-> BooleanAlgebra a -> BooleanAlgebra a
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> BooleanAlgebra a -> c (BooleanAlgebra a)
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c (BooleanAlgebra a)
forall a. Data a => Typeable (BooleanAlgebra a)
forall a. Data a => BooleanAlgebra a -> DataType
forall a. Data a => BooleanAlgebra a -> Constr
forall a.
Data a =>
(forall b. Data b => b -> b)
-> BooleanAlgebra a -> BooleanAlgebra a
forall a u.
Data a =>
Int -> (forall d. Data d => d -> u) -> BooleanAlgebra a -> u
forall a u.
Data a =>
(forall d. Data d => d -> u) -> BooleanAlgebra a -> [u]
forall a r r'.
Data a =>
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> BooleanAlgebra a -> r
forall a r r'.
Data a =>
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> BooleanAlgebra a -> r
forall a (m :: * -> *).
(Data a, Monad m) =>
(forall d. Data d => d -> m d)
-> BooleanAlgebra a -> m (BooleanAlgebra a)
forall a (m :: * -> *).
(Data a, MonadPlus m) =>
(forall d. Data d => d -> m d)
-> BooleanAlgebra a -> m (BooleanAlgebra a)
forall a (c :: * -> *).
Data a =>
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c (BooleanAlgebra a)
forall a (c :: * -> *).
Data a =>
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> BooleanAlgebra a -> c (BooleanAlgebra a)
forall a (t :: * -> *) (c :: * -> *).
(Data a, Typeable t) =>
(forall d. Data d => c (t d)) -> Maybe (c (BooleanAlgebra a))
forall a (t :: * -> * -> *) (c :: * -> *).
(Data a, Typeable t) =>
(forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c (BooleanAlgebra a))
forall a.
Typeable a
-> (forall (c :: * -> *).
    (forall d b. Data d => c (d -> b) -> d -> c b)
    -> (forall g. g -> c g) -> a -> c a)
-> (forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c a)
-> (a -> Constr)
-> (a -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c a))
-> (forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c a))
-> ((forall b. Data b => b -> b) -> a -> a)
-> (forall r r'.
    (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall r r'.
    (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall u. (forall d. Data d => d -> u) -> a -> [u])
-> (forall u. Int -> (forall d. Data d => d -> u) -> a -> u)
-> (forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> Data a
forall u.
Int -> (forall d. Data d => d -> u) -> BooleanAlgebra a -> u
forall u. (forall d. Data d => d -> u) -> BooleanAlgebra a -> [u]
forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> BooleanAlgebra a -> r
forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> BooleanAlgebra a -> r
forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d)
-> BooleanAlgebra a -> m (BooleanAlgebra a)
forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d)
-> BooleanAlgebra a -> m (BooleanAlgebra a)
forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c (BooleanAlgebra a)
forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> BooleanAlgebra a -> c (BooleanAlgebra a)
forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c (BooleanAlgebra a))
forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c (BooleanAlgebra a))
$cBooleanAlgebra :: Constr
$tBooleanAlgebra :: DataType
gmapMo :: (forall d. Data d => d -> m d)
-> BooleanAlgebra a -> m (BooleanAlgebra a)
$cgmapMo :: forall a (m :: * -> *).
(Data a, MonadPlus m) =>
(forall d. Data d => d -> m d)
-> BooleanAlgebra a -> m (BooleanAlgebra a)
gmapMp :: (forall d. Data d => d -> m d)
-> BooleanAlgebra a -> m (BooleanAlgebra a)
$cgmapMp :: forall a (m :: * -> *).
(Data a, MonadPlus m) =>
(forall d. Data d => d -> m d)
-> BooleanAlgebra a -> m (BooleanAlgebra a)
gmapM :: (forall d. Data d => d -> m d)
-> BooleanAlgebra a -> m (BooleanAlgebra a)
$cgmapM :: forall a (m :: * -> *).
(Data a, Monad m) =>
(forall d. Data d => d -> m d)
-> BooleanAlgebra a -> m (BooleanAlgebra a)
gmapQi :: Int -> (forall d. Data d => d -> u) -> BooleanAlgebra a -> u
$cgmapQi :: forall a u.
Data a =>
Int -> (forall d. Data d => d -> u) -> BooleanAlgebra a -> u
gmapQ :: (forall d. Data d => d -> u) -> BooleanAlgebra a -> [u]
$cgmapQ :: forall a u.
Data a =>
(forall d. Data d => d -> u) -> BooleanAlgebra a -> [u]
gmapQr :: (r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> BooleanAlgebra a -> r
$cgmapQr :: forall a r r'.
Data a =>
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> BooleanAlgebra a -> r
gmapQl :: (r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> BooleanAlgebra a -> r
$cgmapQl :: forall a r r'.
Data a =>
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> BooleanAlgebra a -> r
gmapT :: (forall b. Data b => b -> b)
-> BooleanAlgebra a -> BooleanAlgebra a
$cgmapT :: forall a.
Data a =>
(forall b. Data b => b -> b)
-> BooleanAlgebra a -> BooleanAlgebra a
dataCast2 :: (forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c (BooleanAlgebra a))
$cdataCast2 :: forall a (t :: * -> * -> *) (c :: * -> *).
(Data a, Typeable t) =>
(forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c (BooleanAlgebra a))
dataCast1 :: (forall d. Data d => c (t d)) -> Maybe (c (BooleanAlgebra a))
$cdataCast1 :: forall a (t :: * -> *) (c :: * -> *).
(Data a, Typeable t) =>
(forall d. Data d => c (t d)) -> Maybe (c (BooleanAlgebra a))
dataTypeOf :: BooleanAlgebra a -> DataType
$cdataTypeOf :: forall a. Data a => BooleanAlgebra a -> DataType
toConstr :: BooleanAlgebra a -> Constr
$ctoConstr :: forall a. Data a => BooleanAlgebra a -> Constr
gunfold :: (forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c (BooleanAlgebra a)
$cgunfold :: forall a (c :: * -> *).
Data a =>
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c (BooleanAlgebra a)
gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> BooleanAlgebra a -> c (BooleanAlgebra a)
$cgfoldl :: forall a (c :: * -> *).
Data a =>
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> BooleanAlgebra a -> c (BooleanAlgebra a)
$cp1Data :: forall a. Data a => Typeable (BooleanAlgebra a)
Data, (forall x. BooleanAlgebra a -> Rep (BooleanAlgebra a) x)
-> (forall x. Rep (BooleanAlgebra a) x -> BooleanAlgebra a)
-> Generic (BooleanAlgebra a)
forall x. Rep (BooleanAlgebra a) x -> BooleanAlgebra a
forall x. BooleanAlgebra a -> Rep (BooleanAlgebra a) x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
forall a x. Rep (BooleanAlgebra a) x -> BooleanAlgebra a
forall a x. BooleanAlgebra a -> Rep (BooleanAlgebra a) x
$cto :: forall a x. Rep (BooleanAlgebra a) x -> BooleanAlgebra a
$cfrom :: forall a x. BooleanAlgebra a -> Rep (BooleanAlgebra a) x
Generic
    )

instance Heyting a => Boolean (BooleanAlgebra a)

-- |
-- Smart constructro of the @'Boolean'@ type.
boolean :: Heyting a => a -> BooleanAlgebra a
boolean :: a -> BooleanAlgebra a
boolean = a -> BooleanAlgebra a
forall a. a -> BooleanAlgebra a
BooleanAlgebra (a -> BooleanAlgebra a) -> (a -> a) -> a -> BooleanAlgebra a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> a
forall a. Heyting a => a -> a
toBoolean