Idris2Doc : Structures.Collections.PriorityQueue

Structures.Collections.PriorityQueue

Definitions

interface PriorityQueue : (Type -> Type) -> Type
Parameters: queue
Methods:
empty : Ord e => queue e
  Return an empty queue
singleton : Ord e => e -> queue e
  Create a queue containing only one element
isNull : queue e -> Bool
  Return true if the queue is empty
length : queue e -> Nat
  Returns the number of elements in the queue
findMin : queue e -> Maybe e
  Find the minimum element, if there is one
meld : queue e -> queue e -> queue e
  Merge two queues
insert : e -> queue e -> queue e
  Insert an element into the queue
deleteMin : queue e -> queue e
  Removes the minimum element from the queue
Does nothing to the empty queue
fromFoldable : Ord e => Foldable m => m e -> queue e
  Converts an Ord t => Foldable m => m t into a queue of t
queueFoldl : (acc -> e -> acc) -> acc -> queue e -> acc
  Foldl implementation for queues
empty : PriorityQueue queue => Ord e => queue e
  Return an empty queue

Totality: total
Visibility: public export
singleton : PriorityQueue queue => Ord e => e -> queue e
  Create a queue containing only one element

Totality: total
Visibility: public export
isNull : PriorityQueue queue => queue e -> Bool
  Return true if the queue is empty

Totality: total
Visibility: public export
length : PriorityQueue queue => queue e -> Nat
  Returns the number of elements in the queue

Totality: total
Visibility: public export
findMin : PriorityQueue queue => queue e -> Maybe e
  Find the minimum element, if there is one

Totality: total
Visibility: public export
meld : PriorityQueue queue => queue e -> queue e -> queue e
  Merge two queues

Totality: total
Visibility: public export
insert : PriorityQueue queue => e -> queue e -> queue e
  Insert an element into the queue

Totality: total
Visibility: public export
deleteMin : PriorityQueue queue => queue e -> queue e
  Removes the minimum element from the queue
Does nothing to the empty queue

Totality: total
Visibility: public export
fromFoldable : PriorityQueue queue => Ord e => Foldable m => m e -> queue e
  Converts an Ord t => Foldable m => m t into a queue of t

Totality: total
Visibility: public export
queueFoldl : PriorityQueue queue => (acc -> e -> acc) -> acc -> queue e -> acc
  Foldl implementation for queues

Totality: total
Visibility: public export