Bool package:Agda

Representation of Set Bool as a 4-element enum type. All operations in constant time and space. Mimics the interface of Set. Import as: import qualified Agda.Utils.BoolSet as BoolSet import Agda.Utils.BoolSet (BoolSet)

Isomorphic to Set Bool.

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

Boolean algebras.

The standard semiring on Bools.

Retain object when tag is True.

withBool expected f value applies f to the Value when value is a Boolean and fails otherwise.

Error message example

withBool "MyType" f (String "oops")
-- Error: "parsing MyType failed, expected Boolean, but encountered String"

Types isomorphic to Bool.

A known boolean is one we can obtain a singleton for. Concrete values are trivially known.

Singleton for type level booleans.