| Safe Haskell | None |
|---|---|
| Language | Haskell2010 |
Agda.Utils.Boolean
Description
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.
Minimal complete definition
Methods
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.
Minimal complete definition