Agda-2.6.3.20230914: A dependently typed functional programming language and proof assistant
Safe HaskellSafe-Inferred
LanguageHaskell2010

Agda.Utils.VarSet

Description

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

Synopsis

Documentation

union :: IntSet -> IntSet -> IntSet #

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

unions :: Foldable f => f IntSet -> IntSet #

The union of a list of sets.

member :: Key -> IntSet -> Bool #

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

empty :: IntSet #

\(O(1)\). The empty set.

delete :: Key -> IntSet -> IntSet #

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

singleton :: Key -> IntSet #

\(O(1)\). A set of one element.

fromList :: [Key] -> IntSet #

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

toList :: IntSet -> [Key] #

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

toDescList :: IntSet -> [Key] #

\(O(n)\). Convert the set to a descending 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.

null :: IntSet -> Bool #

\(O(1)\). Is the set empty?

intersection :: IntSet -> IntSet -> IntSet #

\(O(n+m)\). The intersection of two sets.

difference :: IntSet -> IntSet -> IntSet #

\(O(n+m)\). Difference between two sets.