		Search-engine friendly clone of the ACL2 documentation.

Binary-append

This binary function implements append, which is a macro in ACL2. See append

The guard for binary-append requires the first argument to be a true-listp.

Function: binary-append

(defun binary-append (x y)
  (declare (xargs :guard (true-listp x)))
  (cond ((endp x) y)
        (t (cons (car x)
                 (binary-append (cdr x) y)))))