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.
