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

Safe Haskell	None
Language	Haskell2010

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

data BoolSet
(\\) :: BoolSet -> BoolSet -> BoolSet
complement :: BoolSet -> BoolSet
delete :: Bool -> BoolSet -> BoolSet
difference :: BoolSet -> BoolSet -> BoolSet
elems :: BoolSet -> [Bool]
empty :: BoolSet
fromList :: [Bool] -> BoolSet
fromAscList :: [Bool] -> BoolSet
fromDistinctAscList :: [Bool] -> BoolSet
insert :: Bool -> BoolSet -> BoolSet
intersection :: BoolSet -> BoolSet -> BoolSet
isSubsetOf :: BoolSet -> BoolSet -> Bool
lookupMin :: BoolSet -> Maybe Bool
member :: Bool -> BoolSet -> Bool
notMember :: Bool -> BoolSet -> Bool
null :: BoolSet -> Bool
singleton :: Bool -> BoolSet
size :: BoolSet -> Int
toList :: BoolSet -> [Bool]
toAscList :: BoolSet -> [Bool]
toSingleton :: BoolSet -> Maybe Bool
total :: BoolSet
union :: BoolSet -> BoolSet -> BoolSet

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 #