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
.
- eList : List α
The enqueue list, which stores elements that have just been pushed (with the most recently enqueued elements at the head).
- dList : List α
The dequeue list, which buffers elements ready to be dequeued (with the head being the next item to be yielded by
dequeue?
).
Instances For
O(1)
. The empty queue.
Equations
Instances For
Equations
- Std.Queue.instEmptyCollection = { emptyCollection := Std.Queue.empty }
Equations
- Std.Queue.instInhabited = { default := ∅ }
O(1)
amortized, O(n)
worst case. Pop an element from the back of the queue,
returning the element and the new queue.
Equations
Instances For
O(n)
. Applies the monadic predicate p
to every element in the queue, and returns the queue
of elements for which p
returns true
. Note that there are currently no guarantees for the order
that p
is applied in.
Equations
- One or more equations did not get rendered due to their size.