Agda.Utils.Boolean

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

Boolean algebras.

Minimal complete definition

fromBool

Methods

fromBool :: Bool -> a

true :: a

false :: a

not :: a -> a

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

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

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

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

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

implies :: a -> a -> a

butNot :: a -> a -> a

Set difference, dual to implies.

Instances

Boolean UnicodeOrAscii

Defined in Agda.Syntax.Concrete.Glyph

Methods

fromBool :: Bool -> UnicodeOrAscii

true :: UnicodeOrAscii

false :: UnicodeOrAscii

not :: UnicodeOrAscii -> UnicodeOrAscii

(&&) :: UnicodeOrAscii -> UnicodeOrAscii -> UnicodeOrAscii

(||) :: UnicodeOrAscii -> UnicodeOrAscii -> UnicodeOrAscii

implies :: UnicodeOrAscii -> UnicodeOrAscii -> UnicodeOrAscii

butNot :: UnicodeOrAscii -> UnicodeOrAscii -> UnicodeOrAscii

Boolean IsFibrant

Defined in Agda.Syntax.Internal.Univ

Methods

fromBool :: Bool -> IsFibrant

true :: IsFibrant

false :: IsFibrant

not :: IsFibrant -> IsFibrant

(&&) :: IsFibrant -> IsFibrant -> IsFibrant

(||) :: IsFibrant -> IsFibrant -> IsFibrant

implies :: IsFibrant -> IsFibrant -> IsFibrant

butNot :: IsFibrant -> IsFibrant -> IsFibrant

Boolean Bool

Defined in Agda.Utils.Boolean

Methods

fromBool :: Bool -> Bool

true :: Bool

false :: Bool

not :: Bool -> Bool

(&&) :: Bool -> Bool -> Bool

(||) :: Bool -> Bool -> Bool

implies :: Bool -> Bool -> Bool

butNot :: Bool -> Bool -> Bool

Boolean b => Boolean (a -> b)

Defined in Agda.Utils.Boolean

Methods

fromBool :: Bool -> a -> b

true :: a -> b

false :: a -> b

not :: (a -> b) -> a -> b

(&&) :: (a -> b) -> (a -> b) -> a -> b

(||) :: (a -> b) -> (a -> b) -> a -> b

implies :: (a -> b) -> (a -> b) -> a -> b

butNot :: (a -> b) -> (a -> b) -> a -> b

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

Types isomorphic to Bool.

Minimal complete definition

toBool

Methods

toBool :: a -> Bool

ifThenElse :: a -> b -> b -> b

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

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

Instances

IsBool UnicodeOrAscii

Defined in Agda.Syntax.Concrete.Glyph

Methods

toBool :: UnicodeOrAscii -> Bool

ifThenElse :: UnicodeOrAscii -> b -> b -> b

fromBool1 :: (Bool -> Bool) -> UnicodeOrAscii -> UnicodeOrAscii

fromBool2 :: (Bool -> Bool -> Bool) -> UnicodeOrAscii -> UnicodeOrAscii -> UnicodeOrAscii

IsBool IsFibrant

Defined in Agda.Syntax.Internal.Univ

Methods

toBool :: IsFibrant -> Bool

ifThenElse :: IsFibrant -> b -> b -> b

fromBool1 :: (Bool -> Bool) -> IsFibrant -> IsFibrant

fromBool2 :: (Bool -> Bool -> Bool) -> IsFibrant -> IsFibrant -> IsFibrant

IsBool Bool

Defined in Agda.Utils.Boolean

Methods

toBool :: Bool -> Bool

ifThenElse :: Bool -> b -> b -> b

fromBool1 :: (Bool -> Bool) -> Bool -> Bool

fromBool2 :: (Bool -> Bool -> Bool) -> Bool -> Bool -> Bool