Agda-2.8.0: A dependently typed functional programming language and proof assistant

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`

Synopsis

- class Boolean a where
  - fromBool :: Bool -> a
  - true :: a
  - false :: a
  - not :: a -> a
  - (&&) :: a -> a -> a
  - (||) :: a -> a -> a
  - implies :: a -> a -> a
  - butNot :: a -> a -> a
- class (Boolean a, Eq a) => IsBool a where
  - toBool :: a -> Bool
  - ifThenElse :: a -> b -> b -> b
  - fromBool1 :: (Bool -> Bool) -> a -> a
  - fromBool2 :: (Bool -> Bool -> Bool) -> a -> a -> a

# Documentation

class Boolean a where Source #

Boolean algebras.

Minimal complete definition

fromBool

Methods

fromBool :: Bool -> a Source #

true :: a Source #

false :: a Source #

not :: a -> a Source #

default not :: IsBool a => a -> a Source #

(&&) :: a -> a -> a infixr 3 Source #

default (&&) :: IsBool a => a -> a -> a Source #

(||) :: a -> a -> a infixr 2 Source #

default (||) :: IsBool a => a -> a -> a Source #

implies :: a -> a -> a Source #

butNot :: a -> a -> a Source #

Set difference, dual to `implies`.

#### Instances

Instances details

Boolean DisplayLHS Source # |

Instance details

Defined in Agda.Syntax.Common

Methods

fromBool :: Bool -> DisplayLHS Source #

true :: DisplayLHS Source #

false :: DisplayLHS Source #

not :: DisplayLHS -> DisplayLHS Source #

(&&) :: DisplayLHS -> DisplayLHS -> DisplayLHS Source #

(||) :: DisplayLHS -> DisplayLHS -> DisplayLHS Source #

implies :: DisplayLHS -> DisplayLHS -> DisplayLHS Source #

butNot :: DisplayLHS -> DisplayLHS -> DisplayLHS Source #

Boolean IsAbstract Source # |

Instance details

Defined in Agda.Syntax.Common

Methods

fromBool :: Bool -> IsAbstract Source #

true :: IsAbstract Source #

false :: IsAbstract Source #

not :: IsAbstract -> IsAbstract Source #

(&&) :: IsAbstract -> IsAbstract -> IsAbstract Source #

(||) :: IsAbstract -> IsAbstract -> IsAbstract Source #

implies :: IsAbstract -> IsAbstract -> IsAbstract Source #

butNot :: IsAbstract -> IsAbstract -> IsAbstract Source #

Boolean UnicodeOrAscii Source # |

Instance details

Defined in Agda.Syntax.Concrete.Glyph

Methods

fromBool :: Bool -> UnicodeOrAscii Source #

true :: UnicodeOrAscii Source #

false :: UnicodeOrAscii Source #

not :: UnicodeOrAscii -> UnicodeOrAscii Source #

(&&) :: UnicodeOrAscii -> UnicodeOrAscii -> UnicodeOrAscii Source #

(||) :: UnicodeOrAscii -> UnicodeOrAscii -> UnicodeOrAscii Source #

implies :: UnicodeOrAscii -> UnicodeOrAscii -> UnicodeOrAscii Source #

butNot :: UnicodeOrAscii -> UnicodeOrAscii -> UnicodeOrAscii Source #

Boolean IsFibrant Source # |

Instance details

Defined in Agda.Syntax.Internal.Univ

Methods

fromBool :: Bool -> IsFibrant Source #

true :: IsFibrant Source #

false :: IsFibrant Source #

not :: IsFibrant -> IsFibrant Source #

(&&) :: IsFibrant -> IsFibrant -> IsFibrant Source #

(||) :: IsFibrant -> IsFibrant -> IsFibrant Source #

implies :: IsFibrant -> IsFibrant -> IsFibrant Source #

butNot :: IsFibrant -> IsFibrant -> IsFibrant Source #

Boolean GuardednessHelps Source # |

Instance details

Defined in Agda.Termination.Termination

Methods

fromBool :: Bool -> GuardednessHelps Source #

true :: GuardednessHelps Source #

false :: GuardednessHelps Source #

not :: GuardednessHelps -> GuardednessHelps Source #

(&&) :: GuardednessHelps -> GuardednessHelps -> GuardednessHelps Source #

(||) :: GuardednessHelps -> GuardednessHelps -> GuardednessHelps Source #

implies :: GuardednessHelps -> GuardednessHelps -> GuardednessHelps Source #

butNot :: GuardednessHelps -> GuardednessHelps -> GuardednessHelps Source #

Boolean Bool Source # |
Instance details Defined in Agda.Utils.Boolean Methods fromBool :: Bool -> Bool Source # true :: Bool Source # false :: Bool Source # not :: Bool -> Bool Source # (&&) :: Bool -> Bool -> Bool Source # (||) :: Bool -> Bool -> Bool Source # implies :: Bool -> Bool -> Bool Source # butNot :: Bool -> Bool -> Bool Source #
Boolean b => Boolean (a -> b) Source # |
Instance details Defined in Agda.Utils.Boolean Methods fromBool :: Bool -> a -> b Source # true :: a -> b Source # false :: a -> b Source # not :: (a -> b) -> a -> b Source # (&&) :: (a -> b) -> (a -> b) -> a -> b Source # (||) :: (a -> b) -> (a -> b) -> a -> b Source # implies :: (a -> b) -> (a -> b) -> a -> b Source # butNot :: (a -> b) -> (a -> b) -> a -> b Source #

class (Boolean a, Eq a) => IsBool a where Source #

Types isomorphic to `Bool`.

Minimal complete definition

toBool

Methods

toBool :: a -> Bool Source #

ifThenElse :: a -> b -> b -> b Source #

fromBool1 :: (Bool -> Bool) -> a -> a Source #

fromBool2 :: (Bool -> Bool -> Bool) -> a -> a -> a Source #

#### Instances

Instances details

IsBool DisplayLHS Source # |
Instance details Defined in Agda.Syntax.Common Methods toBool :: DisplayLHS -> Bool Source # ifThenElse :: DisplayLHS -> b -> b -> b Source # fromBool1 :: (Bool -> Bool) -> DisplayLHS -> DisplayLHS Source # fromBool2 :: (Bool -> Bool -> Bool) -> DisplayLHS -> DisplayLHS -> DisplayLHS Source #
IsBool IsAbstract Source # |
Instance details Defined in Agda.Syntax.Common Methods 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 # |
Instance details Defined in Agda.Syntax.Concrete.Glyph Methods 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 # |
Instance details Defined in Agda.Syntax.Internal.Univ Methods toBool :: IsFibrant -> Bool Source # ifThenElse :: IsFibrant -> b -> b -> b Source # fromBool1 :: (Bool -> Bool) -> IsFibrant -> IsFibrant Source # fromBool2 :: (Bool -> Bool -> Bool) -> IsFibrant -> IsFibrant -> IsFibrant Source #
IsBool GuardednessHelps Source # |
Instance details Defined in Agda.Termination.Termination Methods toBool :: GuardednessHelps -> Bool Source # ifThenElse :: GuardednessHelps -> b -> b -> b Source # fromBool1 :: (Bool -> Bool) -> GuardednessHelps -> GuardednessHelps Source # fromBool2 :: (Bool -> Bool -> Bool) -> GuardednessHelps -> GuardednessHelps -> GuardednessHelps Source #
IsBool Bool Source # |
Instance details Defined in Agda.Utils.Boolean Methods toBool :: Bool -> Bool Source # ifThenElse :: Bool -> b -> b -> b Source # fromBool1 :: (Bool -> Bool) -> Bool -> Bool Source # fromBool2 :: (Bool -> Bool -> Bool) -> Bool -> Bool -> Bool Source #