concatentate the reverse of one list to another
Major Section:  ACL2-BUILT-INS

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

To see the ACL2 definition of this function, see pf.