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



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



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.