Agda-2.6.3.20230914: A dependently typed functional programming language and proof assistant
Safe HaskellSafe-Inferred
LanguageHaskell2010

Agda.Utils.BoolSet

Description

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)

Synopsis

Documentation

data BoolSet Source #

Isomorphic to Set Bool.

Instances

Instances details
Bounded BoolSet Source # 
Instance details

Defined in Agda.Utils.BoolSet

Enum BoolSet Source # 
Instance details

Defined in Agda.Utils.BoolSet

Show BoolSet Source # 
Instance details

Defined in Agda.Utils.BoolSet

Eq BoolSet Source # 
Instance details

Defined in Agda.Utils.BoolSet

Methods

(==) :: BoolSet -> BoolSet -> Bool #

(/=) :: BoolSet -> BoolSet -> Bool #

Ord BoolSet Source # 
Instance details

Defined in Agda.Utils.BoolSet

empty :: BoolSet Source #

The empty set.

notMember :: Bool -> BoolSet -> Bool Source #

not . member b.

singleton :: Bool -> BoolSet Source #

A singleton set.

toSingleton :: BoolSet -> Maybe Bool Source #

toSingleton s == Just b iff s == singleton b.

total :: BoolSet Source #

The full set.