Data.Map.Internal

Map Internals

Definitions

Size : Type

Totality: total
Visibility: public export

data Map : Type -> Type -> Type

  A finite map from keys k to values v.

Totality: total
Visibility: public export
Constructors:

Bin : Size -> k -> v -> Map k v -> Map k v -> Map k v

Tip : Map k v

Hints:

Eq k => Eq v => Eq (Map k v)

Foldable (Map k)

Functor (Map k)

Ord k => Ord v => Ord (Map k v)

Show k => Show v => Show (Map k v)

Show (List (k, v)) => Show (Map k v)

data MinView : Type -> Type -> Type

Totality: total
Visibility: public export
Constructor: 

MinView' : k -> a -> Map k a -> MinView k a

Hints:

Eq {arg:13044} => Eq {arg:13048} => Eq (MinView {arg:13044} {arg:13048})

Ord {arg:13044} => Ord {arg:13048} => Ord (MinView {arg:13044} {arg:13048})

Show {arg:13044} => Show {arg:13048} => Show (MinView {arg:13044} {arg:13048})

data MaxView : Type -> Type -> Type

Totality: total
Visibility: public export
Constructor: 

MaxView' : k -> a -> Map k a -> MaxView k a

Hints:

Eq {arg:13479} => Eq {arg:13483} => Eq (MaxView {arg:13479} {arg:13483})

Ord {arg:13479} => Ord {arg:13483} => Ord (MaxView {arg:13479} {arg:13483})

Show {arg:13479} => Show {arg:13483} => Show (MaxView {arg:13479} {arg:13483})

singleton : k -> a -> Map k a

  Wrap a single value in a map.

Totality: total
Visibility: export

size : Map k v -> Nat

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

Totality: total
Visibility: export

balance : k -> v -> Map k v -> Map k v -> Map k v

  Balances a map after the addition, deletion, or updating of a map via a new key and value.

Totality: total
Visibility: export

balanceL : k -> v -> Map k v -> Map k v -> Map k v

  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 : k -> v -> Map k v -> Map k v -> Map k v

  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 : k -> v -> Map k v -> Map k v

Totality: total
Visibility: export

insertMin : k -> v -> Map k v -> Map k v

Totality: total
Visibility: export

minViewSure : k -> v -> Map k v -> Map k v -> MinView k v

Totality: total
Visibility: export

maxViewSure : k -> v -> Map k v -> Map k v -> MaxView k v

Totality: total
Visibility: export

glue : Map k v -> Map k v -> Map k v

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

Totality: total
Visibility: export

link2 : Map k v -> Map k v -> Map k v

  Utility function that maintains the balance properties of the tree.

Totality: total
Visibility: export

link : k -> v -> Map k v -> Map k v -> Map k v

  Utility function that maintains the balance properties of the tree.

Totality: total
Visibility: export