Source code in the acl2 programming language

(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))