Data.Set.Internal

(source)

Set Internals

Definitions

Size : Type

Totality: total
Visibility: public export

data Set : Type -> Type

  A finite set of values.

Totality: total
Visibility: public export
Constructors:

Bin : Size -> a -> Set a -> Set a -> Set a
Tip : Set a

Hints:

Eq a => Eq (Set a)
Functor Set
Ord a => Ord (Set a)
Show a => Show (Set a)
Show (List a) => Show (Set a)

singleton : a -> Set a

  Wrap a single value in a set.

Totality: total
Visibility: export

size : Set a -> Nat

  The number of elements in the set. O(1)

Totality: total
Visibility: export

delta : Nat

Totality: total
Visibility: export

balanceL : a -> Set a -> Set a -> Set a

  A specialized version of balance.
  balanceL is called when left subtree might have been inserted to or when
  right subtree might have been deleted from.

Totality: total
Visibility: export

balanceR : a -> Set a -> Set a -> Set a

  A specialized version of balance.
  balanceR is called when right subtree might have been inserted to or when
  left subtree might have been deleted from.

Totality: total
Visibility: export

insertMax : a -> Set a -> Set a

Totality: total
Visibility: export

insertMin : a -> Set a -> Set a

Totality: total
Visibility: export

minViewSure : a -> Set a -> Set a -> (a, Set a)

Totality: total
Visibility: export

maxViewSure : a -> Set a -> Set a -> (a, Set a)

Totality: total
Visibility: export

glue : Set a -> Set a -> Set a

  Glues two sets together (assumes that both sets are already balanced with respect to each other).

Totality: total
Visibility: export

link : a -> Set a -> Set a -> Set a

  Utility function that maintains the balance properties of the tree.

Totality: total
Visibility: export