Safe Haskell | None |
---|---|
Language | Haskell2010 |
Boolean algebras and types isomorphic to Bool
.
There are already solutions for Boolean
algebras in the Haskell ecosystem,
but they do not offer easy instantiations for types isomorphic to Bool
.
In particular, if type a
is isomorphic to Bool
, so it satisfies `IsBool a`,
we would like to instantiate 'Boolean a' by just giving true
and false
.
To facilitate this within the limits of the Haskell class system,
we define the class Boolean
mutually with class IsBool
,
so that operations not
, (&&)
, and (||)
can get default implementations.
Usage:
import Prelude hiding ( not, (&&), (||) )
import Agda.Utils.Boolean
Documentation
class Boolean a where Source #
Boolean algebras.
fromBool :: Bool -> a Source #
(&&) :: a -> a -> a infixr 3 Source #
(||) :: a -> a -> a infixr 2 Source #
implies :: a -> a -> a Source #
butNot :: a -> a -> a Source #
Set difference, dual to implies
.
Instances
class (Boolean a, Eq a) => IsBool a where Source #
Types isomorphic to Bool
.
Instances
IsBool IsAbstract Source # | |
Defined in Agda.Syntax.Common toBool :: IsAbstract -> Bool Source # ifThenElse :: IsAbstract -> b -> b -> b Source # fromBool1 :: (Bool -> Bool) -> IsAbstract -> IsAbstract Source # fromBool2 :: (Bool -> Bool -> Bool) -> IsAbstract -> IsAbstract -> IsAbstract Source # | |
IsBool UnicodeOrAscii Source # | |
Defined in Agda.Syntax.Concrete.Glyph toBool :: UnicodeOrAscii -> Bool Source # ifThenElse :: UnicodeOrAscii -> b -> b -> b Source # fromBool1 :: (Bool -> Bool) -> UnicodeOrAscii -> UnicodeOrAscii Source # fromBool2 :: (Bool -> Bool -> Bool) -> UnicodeOrAscii -> UnicodeOrAscii -> UnicodeOrAscii Source # | |
IsBool IsFibrant Source # | |
IsBool Bool Source # | |