		Search-engine friendly clone of the ACL2 documentation.

Hons-revappend

REVAPPEND using HONS instead of CONS

Definitions and Theorems

Function: hons-revappend

(defun hons-revappend (x y)
  (declare (xargs :guard t))
  (mbe :logic (revappend x y)
       :exec
       (if (atom x)
           y
         (hons-revappend (cdr x)
                         (hons (car x) y)))))