		Search-engine friendly clone of the ACL2 documentation.

Svex-focused-equivalence-checking

My-binary-append

Signature
(my-binary-append x y) → *
Arguments: x — Guard (true-listp x).

Definitions and Theorems

Function: my-binary-append

(defun my-binary-append (x y)
  (declare (xargs :guard (true-listp x)))
  (let ((__function__ 'my-binary-append))
    (declare (ignorable __function__))
    (mbe :logic (binary-append x y)
         :exec (if (eq y nil) x (binary-append x y)))))