Agda-2.6.20240714: A dependently typed functional programming language and proof assistant
Safe HaskellNone
LanguageHaskell2010

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

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

Boolean UnicodeOrAscii Source # 
Instance details

Defined in Agda.Syntax.Concrete.Glyph

Boolean IsFibrant Source # 
Instance details

Defined in Agda.Syntax.Internal.Univ

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 #