Structures.Collections.PriorityQueue.BinomialQueue

Definitions

record BinomialQueue : Type -> Type

  A binomial queue per Optimal purely functional priority queues
  (Brodal, G. S., & Okasaki, C. (1996).)

Totality: total
Visibility: export
Constructor: 

MkBQ : Ord e -> (forest_size : Nat) -> Vect forest_size (BinomialPair e) -> BinomialQueue e

Projections:

.forest : ({rec:0} : BinomialQueue e) -> Vect (forest_size {rec:0}) (BinomialPair e)

.forest_size : BinomialQueue e -> Nat

.o : BinomialQueue e -> Ord e

Hint: 

PriorityQueue BinomialQueue