		Search-engine friendly clone of the ACL2 documentation.

Revappend

Concatenate the reverse of one list to another

(Revappend x y) concatenates the reverse of the list x to y, which is also typically a list.

The following theorem characterizes this English description.

(equal (revappend x y)
       (append (reverse x) y))

Hint: This lemma follows immediately from the definition of reverse and the following lemma.

(defthm revappend-append
  (equal (append (revappend x y) z)
         (revappend x (append y z))))

The guard for (revappend x y) requires that x is a true list.

Revappend is defined in Common Lisp. See any Common Lisp documentation for more information.

Function: revappend

(defun revappend (x y)
  (declare (xargs :guard (true-listp x)))
  (if (endp x)
      y
    (revappend (cdr x) (cons (car x) y))))

Std/lists/revappend: Lemmas about revappend available in the std/lists library.
Hons-revappend: REVAPPEND using HONS instead of CONS