structure Std.Queue (α : Type u) :
  • The enqueue list, which stores elements that have just been pushed (with the most recently enqueued elements at the head).

    eList : List α
  • The dequeue list, which buffers elements ready to be dequeued (with the head being the next item to be yielded by dequeue?).

    dList : List α

A functional queue data structure, using two back-to-back lists. If we think of the queue as having elements pushed on the front and popped from the back, then the queue itself is effectively eList ++ dList.reverse.

Instances For
    def Std.Queue.empty {α : Type u} :

    O(1). The empty queue.

    • Std.Queue.empty = { eList := [], dList := [] }
    • Std.Queue.instEmptyCollectionQueue = { emptyCollection := Std.Queue.empty }
    • Std.Queue.instInhabitedQueue = { default := }
    def Std.Queue.isEmpty {α : Type u} (q : Std.Queue α) :

    O(1). Is the queue empty?

    def Std.Queue.enqueue {α : Type u} (v : α) (q : Std.Queue α) :

    O(1). Push an element on the front of the queue.

    def Std.Queue.enqueueAll {α : Type u} (vs : List α) (q : Std.Queue α) :

    O(|vs|). Push a list of elements vs on the front of the queue.

    def Std.Queue.dequeue? {α : Type u} (q : Std.Queue α) :

    O(1) amortized, O(n) worst case. Pop an element from the back of the queue, returning the element and the new queue.

    • One or more equations did not get rendered due to their size.