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

Methods

minBound :: BoolSet #

maxBound :: BoolSet #

Enum BoolSet Source # 
Instance details

Defined in Agda.Utils.BoolSet

Methods

succ :: BoolSet -> BoolSet #

pred :: BoolSet -> BoolSet #

toEnum :: Int -> BoolSet #

fromEnum :: BoolSet -> Int #

enumFrom :: BoolSet -> [BoolSet] #

enumFromThen :: BoolSet -> BoolSet -> [BoolSet] #

enumFromTo :: BoolSet -> BoolSet -> [BoolSet] #

enumFromThenTo :: BoolSet -> BoolSet -> BoolSet -> [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 #

(\\) :: BoolSet -> BoolSet -> BoolSet Source #

complement :: BoolSet -> BoolSet Source #

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

difference :: BoolSet -> BoolSet -> BoolSet Source #

elems :: BoolSet -> [Bool] Source #

empty :: BoolSet Source #

The empty set.

fromList :: [Bool] -> BoolSet Source #

fromAscList :: [Bool] -> BoolSet Source #

fromDistinctAscList :: [Bool] -> BoolSet Source #

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

intersection :: BoolSet -> BoolSet -> BoolSet Source #

isSubsetOf :: BoolSet -> BoolSet -> Bool Source #

lookupMin :: BoolSet -> Maybe Bool 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.

union :: BoolSet -> BoolSet -> BoolSet Source #