Agda-2.8.0: 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 Source # maxBound :: BoolSet Source #
Enum BoolSet Source # |

Instance details

Defined in Agda.Utils.BoolSet

Methods

succ :: BoolSet -> BoolSet Source #

pred :: BoolSet -> BoolSet Source #

toEnum :: Int -> BoolSet Source #

fromEnum :: BoolSet -> Int Source #

enumFrom :: BoolSet -> [BoolSet] Source #

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

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

enumFromThenTo :: BoolSet -> BoolSet -> BoolSet -> [BoolSet] Source #

Show BoolSet Source # |
Instance details Defined in Agda.Utils.BoolSet Methods showsPrec :: Int -> BoolSet -> ShowS Source # show :: BoolSet -> String Source # showList :: [BoolSet] -> ShowS Source #
Eq BoolSet Source # |
Instance details Defined in Agda.Utils.BoolSet Methods (==) :: BoolSet -> BoolSet -> Bool Source # (/=) :: BoolSet -> BoolSet -> Bool Source #
Ord BoolSet Source # |
Instance details Defined in Agda.Utils.BoolSet Methods compare :: BoolSet -> BoolSet -> Ordering Source # (<) :: BoolSet -> BoolSet -> Bool Source # (<=) :: BoolSet -> BoolSet -> Bool Source # (>) :: BoolSet -> BoolSet -> Bool Source # (>=) :: BoolSet -> BoolSet -> Bool Source # max :: BoolSet -> BoolSet -> BoolSet Source # min :: BoolSet -> BoolSet -> BoolSet Source #

(\\) :: 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 #