Agda-2.6.20240714: A dependently typed functional programming language and proof assistant
Safe HaskellNone
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

Methods

showsPrec :: Int -> BoolSet -> ShowS

show :: BoolSet -> String

showList :: [BoolSet] -> ShowS

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

Methods

compare :: BoolSet -> BoolSet -> Ordering

(<) :: BoolSet -> BoolSet -> Bool

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

(>) :: BoolSet -> BoolSet -> Bool

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

max :: BoolSet -> BoolSet -> BoolSet

min :: BoolSet -> BoolSet -> BoolSet

delete :: Bool -> BoolSet -> BoolSet Source #

elems :: BoolSet -> [Bool] Source #

empty :: BoolSet Source #

The empty set.

fromList :: [Bool] -> BoolSet Source #

insert :: Bool -> BoolSet -> BoolSet Source #

member :: Bool -> BoolSet -> Bool Source #

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

not . member b.

null :: BoolSet -> Bool Source #

singleton :: Bool -> BoolSet Source #

A singleton set.

size :: BoolSet -> Int Source #

toList :: BoolSet -> [Bool] Source #

toAscList :: BoolSet -> [Bool] Source #

toSingleton :: BoolSet -> Maybe Bool Source #

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

total :: BoolSet Source #

The full set.