Idris2Doc : Data.Set

Data.Set

(source)
Finite Sets

Reexports

importpublic Data.Set.Internal

Definitions

empty : Seta
  The empty set. O(1)

Totality: total
Visibility: export
foldl : (a->b->a) ->a->Setb->a
  Fold the values in the set using the given left-associative binary operator. O(n)

Totality: total
Visibility: export
foldr : (a->b->b) ->b->Seta->b
  Fold the values in the set using the given right-associative binary operator. O(n)

Totality: total
Visibility: export
insert : Orda=>a->Seta->Seta
  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: export
delete : Orda=>a->Seta->Seta
  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: export
member : Orda=>a->Seta->Bool
  Is the element in the set? O(log n)

Totality: total
Visibility: export
notMember : Orda=>a->Seta->Bool
  Is the element not in the set? O(log n)

Totality: total
Visibility: export
lookupLT : Orda=>a->Seta->Maybea
  Find largest element smaller than the given one. O(log n)

Totality: total
Visibility: export
lookupGT : Orda=>a->Seta->Maybea
  Find smallest element greater than the given one. O(log n)

Totality: total
Visibility: export
lookupLE : Orda=>a->Seta->Maybea
  Find the largest element smaller or equal to the given one. O(log n)

Totality: total
Visibility: export
lookupGE : Orda=>a->Seta->Maybea
  Find the smallest element greater or equal to the given one. O(log n)

Totality: total
Visibility: export
null : Seta->Bool
  Is the set empty? O(1)

Totality: total
Visibility: export
splitMember : Orda=>a->Seta-> (Seta, (Bool, Seta))
  Performs a split but also returns whether
the pivot element was found in the original set. O(log n)

Totality: total
Visibility: export
splitRoot : Seta->List (Seta)
  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: export
split : Orda=>a->Seta-> (Seta, Seta)
  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: export
isSubsetOf : Orda=>Seta->Seta->Bool
  Indicates whether s1 is a subset of s2.

Totality: total
Visibility: export
isProperSubsetOf : Orda=>Seta->Seta->Bool
  Indicates whether s1 is a proper subset of s2.

Totality: total
Visibility: export
disjoint : Orda=>Seta->Seta->Bool
  Check whether two sets are disjoint (i.e. their intersection is empty).

Totality: total
Visibility: export
filter : Eq (Seta) => (a->Bool) ->Seta->Seta
  Filter all elements that satisfy the predicate. O(n)

Totality: total
Visibility: export
takeWhileAntitone : (a->Bool) ->Seta->Seta
  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: export
dropWhileAntitone : (a->Bool) ->Seta->Seta
  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: export
spanAntitone : (a->Bool) ->Seta-> (Seta, Seta)
  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: export
lookupIndex : Orda=>a->Seta->MaybeNat
  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: export
findIndex : Orda=>a->Seta->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: export
elemAt : Nat->Seta->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: export
deleteAt : Nat->Seta->Seta
  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: export
take : Nat->Seta->Seta
  Take a given number of elements in order, beginning
with the smallest keys. O(log n)

Totality: total
Visibility: export
drop : Nat->Seta->Seta
  Drop a given number of elements in order, beginning
with the smallest ones. O(log n)

Totality: total
Visibility: export
splitAt : Nat->Seta-> (Seta, Seta)
  Split a set at a particular index. O(log n)

Totality: total
Visibility: export
lookupMin : Seta->Maybea
  The minimal element of the set. Returns Nothing if the set is empty. O(log n)

Totality: total
Visibility: export
lookupMax : Seta->Maybea
  The maximal element of the set. Returns Nothing if the set is empty. O(log n)

Totality: total
Visibility: export
findMin : Seta->a
  The minimal element of the set. Calls idris_crash if the set is empty. O(log n)

Totality: total
Visibility: export
findMax : Seta->a
  The maximal element of the set. Calls idris_crash if the set is empty. O(log n)

Totality: total
Visibility: export
deleteMin : Seta->Seta
  Delete the minimal element. Returns an empty set if the set is empty. O(log n)

Totality: total
Visibility: export
deleteMax : Seta->Seta
  Delete the maximal element. Returns an empty set if the set is empty. O(log n)

Totality: total
Visibility: export
minView : Seta->Maybe (a, Seta)
  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: export
deleteFindMin : Seta-> (a, Seta)
  Delete and find the minimal element. O(log n)

Totality: total
Visibility: export
maxView : Seta->Maybe (a, Seta)
  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: export
deleteFindMax : Seta-> (a, Seta)
  Delete and find the maximal element. O(log n)

Totality: total
Visibility: export
union : Eq (Seta) =>Eqa=>Orda=>Seta->Seta->Seta
  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: export
difference : Orda=>Seta->Seta->Seta
  Difference of two sets.
Return elements of the first set not existing in the second set.

Totality: total
Visibility: export
(\\) : Orda=>Seta->Seta->Seta
  Same as difference.

Totality: total
Visibility: export
Fixity Declaration: infix operator, level 7
intersection : Eq (Seta) =>Orda=>Seta->Seta->Seta
  Intersection of two sets.
Return data in the first set for elements existing in both sets.

Totality: total
Visibility: export
toDescList : Seta->Lista
  Convert the set to a list of elements where the elements are in descending order. O(n)

Totality: total
Visibility: export
toAscList : Seta->Lista
  Convert the set to a list of elements where the elements are in ascending order. O(n)

Totality: total
Visibility: export
toList : Seta->Lista
  Convert the set to a list of elements.

Totality: total
Visibility: export
fromList : Orda=>Lista->Seta
  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: export
map : (a->b) ->Seta->Setb
  Map a function over all elements in the set. O(n)

Totality: total
Visibility: export
disjointUnion : Seta->Setb->Set (Eitherab)
  Calculate the disjoint union of two sets. O(n + m)

Totality: total
Visibility: export