Structures.Collections.PriorityQueue.SkewBinomialQueue

Definitions

record SkewBinomialQueue : Type -> Type

  A binomial queue per Optimal purely functional priority queues
  (Brodal, G. S., & Okasaki, C. (1996).)
  
  Slightly more complicated than a `BinomialQueue`, but supports inserts in
  constant time

Totality: total
Visibility: export
Constructor: 

MkSBQ : Ord e -> (forest_size : Nat) -> Vect forest_size (SkewBinomialPair e) -> SkewBinomialQueue e

Projections:

.forest : ({rec:0} : SkewBinomialQueue e) -> Vect (forest_size {rec:0}) (SkewBinomialPair e)

.forest_size : SkewBinomialQueue e -> Nat

.o : SkewBinomialQueue e -> Ord e

Hint: 

PriorityQueue SkewBinomialQueue