empty : Set a The empty set. O(1)
Totality: total
Visibility: exportfoldl : (a -> b -> a) -> a -> Set b -> a Fold the values in the set using the given left-associative binary operator. O(n)
Totality: total
Visibility: exportfoldr : (a -> b -> b) -> b -> Set a -> b Fold the values in the set using the given right-associative binary operator. O(n)
Totality: total
Visibility: exportinsert : Ord a => a -> Set a -> Set a Insert an element in a set.
If the set already contains an element equal to the given value,
it is replaced with the new value. O(log n)
Totality: total
Visibility: exportdelete : Ord a => a -> Set a -> Set a Delete an element from a set. When the element is not
a member of the set, the original set is returned. O(log n)
Totality: total
Visibility: exportmember : Ord a => a -> Set a -> Bool Is the element in the set? O(log n)
Totality: total
Visibility: exportnotMember : Ord a => a -> Set a -> Bool Is the element not in the set? O(log n)
Totality: total
Visibility: exportlookupLT : Ord a => a -> Set a -> Maybe a Find largest element smaller than the given one. O(log n)
Totality: total
Visibility: exportlookupGT : Ord a => a -> Set a -> Maybe a Find smallest element greater than the given one. O(log n)
Totality: total
Visibility: exportlookupLE : Ord a => a -> Set a -> Maybe a Find the largest element smaller or equal to the given one. O(log n)
Totality: total
Visibility: exportlookupGE : Ord a => a -> Set a -> Maybe a Find the smallest element greater or equal to the given one. O(log n)
Totality: total
Visibility: exportnull : Set a -> Bool Is the set empty? O(1)
Totality: total
Visibility: exportsplitMember : Ord a => a -> Set a -> (Set a, (Bool, Set a)) Performs a split but also returns whether
the pivot element was found in the original set. O(log n)
Totality: total
Visibility: exportsplitRoot : Set a -> List (Set a) Decompose a set into pieces based on the structure of the underlying tree.
This function is useful for consuming a set in parallel. O(1)
Totality: total
Visibility: exportsplit : Ord a => a -> Set a -> (Set a, Set a) The expression (split x set) is a pair (set1,set2) where
set1 comprises the elements of set less than x and
set2 comprises the elements of set greater than x. O(log n)
Totality: total
Visibility: exportisSubsetOf : Ord a => Set a -> Set a -> Bool Indicates whether s1 is a subset of s2.
Totality: total
Visibility: exportisProperSubsetOf : Ord a => Set a -> Set a -> Bool Indicates whether s1 is a proper subset of s2.
Totality: total
Visibility: exportdisjoint : Ord a => Set a -> Set a -> Bool Check whether two sets are disjoint (i.e. their intersection is empty).
Totality: total
Visibility: exportfilter : Eq (Set a) => (a -> Bool) -> Set a -> Set a Filter all elements that satisfy the predicate. O(n)
Totality: total
Visibility: exporttakeWhileAntitone : (a -> Bool) -> Set a -> Set a Take while a predicate on the keys holds.
The user is responsible for ensuring that for all elements j and k in the set,
j < k ==> p j >= p k. See note at spanAntitone. O(log n)
Totality: total
Visibility: exportdropWhileAntitone : (a -> Bool) -> Set a -> Set a Drop while a predicate on the keys holds.
The user is responsible for ensuring that for all elements j and k in the map,
j < k ==> p j >= p k. See note at spanAntitone. O(log n)
Totality: total
Visibility: exportspanAntitone : (a -> Bool) -> Set a -> (Set a, Set a) Divide a map at the point where a predicate on the keys stops holding.
The user is responsible for ensuring that for all keys j and k in the map,
j < k ==> p j>= p k. O(log n)
Totality: total
Visibility: exportlookupIndex : Ord a => a -> Set a -> Maybe Nat Lookup the index of a element, which is its zero-based index in
the sorted sequence of elements. The index is a number from 0 up to, but not
including, the size of the set. O(log n)
Totality: total
Visibility: exportfindIndex : Ord a => a -> Set a -> Nat Return the index of an element, which is its zero-based index in
the sorted sequence of elements. The index is a number from 0 up to, but not
including, the size of the set. Calls idris_crash when the element is not
a member of the set. O(log n)
Totality: total
Visibility: exportelemAt : Nat -> Set a -> a Retrieve an element by its index, i.e. by its zero-based
index in the sorted sequence of elements. If the index is out of range (less
than zero, greater or equal to size of the set), idris_crash is called. O(log n)
Totality: total
Visibility: exportdeleteAt : Nat -> Set a -> Set a Delete the element at index, i.e. by its zero-based index in
the sorted sequence of elements. If the index is out of range (less than zero,
greater or equal to size of the set), idris_crash is called. O(log n)
Totality: total
Visibility: exporttake : Nat -> Set a -> Set a Take a given number of elements in order, beginning
with the smallest keys. O(log n)
Totality: total
Visibility: exportdrop : Nat -> Set a -> Set a Drop a given number of elements in order, beginning
with the smallest ones. O(log n)
Totality: total
Visibility: exportsplitAt : Nat -> Set a -> (Set a, Set a) Split a set at a particular index. O(log n)
Totality: total
Visibility: exportlookupMin : Set a -> Maybe a The minimal element of the set. Returns Nothing if the set is empty. O(log n)
Totality: total
Visibility: exportlookupMax : Set a -> Maybe a The maximal element of the set. Returns Nothing if the set is empty. O(log n)
Totality: total
Visibility: exportfindMin : Set a -> a The minimal element of the set. Calls idris_crash if the set is empty. O(log n)
Totality: total
Visibility: exportfindMax : Set a -> a The maximal element of the set. Calls idris_crash if the set is empty. O(log n)
Totality: total
Visibility: exportdeleteMin : Set a -> Set a Delete the minimal element. Returns an empty set if the set is empty. O(log n)
Totality: total
Visibility: exportdeleteMax : Set a -> Set a Delete the maximal element. Returns an empty set if the set is empty. O(log n)
Totality: total
Visibility: exportminView : Set a -> Maybe (a, Set a) Retrieves the minimal element of the set, and
the set stripped of that element, or Nothing if passed an empty set. O(log n)
Totality: total
Visibility: exportdeleteFindMin : Set a -> (a, Set a) Delete and find the minimal element. O(log n)
Totality: total
Visibility: exportmaxView : Set a -> Maybe (a, Set a) Retrieves the maximal element of the set, and
the set stripped of that element, or Nothing if passed an empty set. O(log n)
Totality: total
Visibility: exportdeleteFindMax : Set a -> (a, Set a) Delete and find the maximal element. O(log n)
Totality: total
Visibility: exportunion : Eq (Set a) => Eq a => Ord a => Set a -> Set a -> Set a The expression (union t1 t2) takes the left-biased union of t1 and t2.
It prefers t1 when duplicate keys are encountered.
Totality: total
Visibility: exportdifference : Ord a => Set a -> Set a -> Set a Difference of two sets.
Return elements of the first set not existing in the second set.
Totality: total
Visibility: export(\\) : Ord a => Set a -> Set a -> Set a Same as difference.
Totality: total
Visibility: export
Fixity Declaration: infix operator, level 7intersection : Eq (Set a) => Ord a => Set a -> Set a -> Set a Intersection of two sets.
Return data in the first set for elements existing in both sets.
Totality: total
Visibility: exporttoDescList : Set a -> List a Convert the set to a list of elements where the elements are in descending order. O(n)
Totality: total
Visibility: exporttoAscList : Set a -> List a Convert the set to a list of elements where the elements are in ascending order. O(n)
Totality: total
Visibility: exporttoList : Set a -> List a Convert the set to a list of elements.
Totality: total
Visibility: exportfromList : Ord a => List a -> Set a Build a set from a list of elements.
If the list contains identical element(s),
the last of each identical elemen is retained.
If the elements of the list are ordered, a linear-time implementation is used. O(n * log(n))
Totality: total
Visibility: exportmap : (a -> b) -> Set a -> Set b Map a function over all elements in the set. O(n)
Totality: total
Visibility: exportdisjointUnion : Set a -> Set b -> Set (Either a b) Calculate the disjoint union of two sets. O(n + m)
Totality: total
Visibility: export