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

Safe Haskell | Safe-Infered

Agda.Utils.VarSet

Description

Var field implementation of sets of (small) natural numbers.

Synopsis

- type VarSet = Set Integer
- union :: Ord a => Set a -> Set a -> Set a
- unions :: Ord a => [Set a] -> Set a
- member :: Ord a => a -> Set a -> Bool
- empty :: Set a
- delete :: Ord a => a -> Set a -> Set a
- singleton :: a -> Set a
- fromList :: Ord a => [a] -> Set a
- toList :: Set a -> [a]
- isSubsetOf :: Ord a => Set a -> Set a -> Bool
- subtract :: Integer -> VarSet -> VarSet

# Documentation

type VarSet = Set Integer

union :: Ord a => Set a -> Set a -> Set a

O(n+m). The union of two sets, preferring the first set when equal elements are encountered. The implementation uses the efficient hedge-union algorithm. Hedge-union is more efficient on (bigset `union` smallset).

unions :: Ord a => [Set a] -> Set a

The union of a list of sets: (``unions` == `foldl` `union` `empty``).

member :: Ord a => a -> Set a -> Bool

O(log n). Is the element in the set?

empty :: Set a

O(1). The empty set.

delete :: Ord a => a -> Set a -> Set a

O(log n). Delete an element from a set.

singleton :: a -> Set a

O(1). Create a singleton set.

fromList :: Ord a => [a] -> Set a

O(n*log n). Create a set from a list of elements.

toList :: Set a -> [a]

O(n). Convert the set to a list of elements.

isSubsetOf :: Ord a => Set a -> Set a -> Bool

O(n+m). Is this a subset? `(s1 `isSubsetOf` s2)` tells whether `s1` is a subset of `s2`.

subtract :: Integer -> VarSet -> VarSet