Agda- A dependently typed functional programming language and proof assistant

Safe HaskellSafe-Inferred



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



union :: IntSet -> IntSet -> IntSet

O(n+m). The union of two sets.

unions :: [IntSet] -> IntSet

The union of a list of sets.

member :: Int -> IntSet -> Bool

O(min(n,W)). Is the value a member of the set?

empty :: IntSet

O(1). The empty set.

delete :: Int -> IntSet -> IntSet

O(min(n,W)). Delete a value in the set. Returns the original set when the value was not present.

singleton :: Int -> IntSet

O(1). A set of one element.

fromList :: [Int] -> IntSet

O(n*min(n,W)). Create a set from a list of integers.

toList :: IntSet -> [Int]

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

isSubsetOf :: IntSet -> IntSet -> Bool

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