|
(defun enqueue (x xs)
|
|
(cons x xs))
|
|
|
|
(defun dequeue (xs)
|
|
(declare (xargs :guard (and (consp xs)
|
|
(true-listp xs))))
|
|
(if (or (endp xs) (endp (rest xs)))
|
|
(mv (first xs) nil)
|
|
(mv-let (x ys)
|
|
(dequeue (rest xs))
|
|
(mv x (cons (first xs) ys)))))
|
|
|
|
(defun empty (xs)
|
|
(endp xs))
|