Agda.Utils.VarSet

O(1). The empty set.

O(\min(n,W)). Add a value to the set. There is no left- or right bias for IntSets.

O(1). A set of one element.

O(\min(n, m \log \frac{2^W}{m})), m \leq n. The union of two sets.

The union of a list of sets.

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

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

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

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

O(\min(n, m \log \frac{2^W}{m})), m \leq n. Check whether two sets are disjoint (i.e. their intersection is empty).

disjoint (fromList [2,4,6])   (fromList [1,3])     == True
disjoint (fromList [2,4,6,8]) (fromList [2,3,5,7]) == False
disjoint (fromList [1,2])     (fromList [1,2,3,4]) == False
disjoint (fromList [])        (fromList [])        == True

O(\min(n, m \log \frac{2^W}{m})), m \leq n. Is this a subset? (s1 `isSubsetOf` s2) tells whether s1 is a subset of s2.

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

O(1). Is the set empty?

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

O(\min(n, m \log \frac{2^W}{m})), m \leq n. Difference between two sets.

O(n). Filter all elements that satisfy some predicate.

Keep only elements greater or equal to the given pivot.

O(\min(n, m \log \frac{2^W}{m})), m \leq n. The intersection of two sets.

O(n). The

mapMonotonic f s == map f s, but works only when f is strictly increasing. Semi-formally, we have:

and [x < y ==> f x < f y | x <- ls, y <- ls]
                    ==> mapMonotonic f s == map f s
    where ls = toList s

Warning: This function should be used only if f is monotonically strictly increasing. This precondition is not checked. Use map if the precondition may not hold.

Subtract from each element.