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 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 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 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 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 #