Major Section: ACL2-BUILT-INS
(Revappend x y) concatenates the reverse of the list
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
reverseand 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.