Reverse a list or string
(Reverse x) is the result of reversing the order of the
elements of the list or string x.
The guard for reverse requires that its argument is a true list
or a string.
Reverse is defined in Common Lisp. See any Common Lisp documentation
for more information.
(defun reverse (x)
(declare (xargs :guard (or (true-listp x) (stringp x))))
(cond ((stringp x)
(coerce (revappend (coerce x 'list) nil)
(t (revappend x nil))))
- A safe mechanism for implementing something like nreverse, for
writing tail-recursive functions that use less memory by avoiding the final
- Logically simple alternative to reverse for lists.
- Lemmas about reverse available in the std/lists
- REVERSE using HONS instead of CONS