		Search-engine friendly clone of the ACL2 documentation.

Utilities

Remove-equal-without-guard

Same as remove-equal, but doesn't require true-listp.

Signature
(remove-equal-without-guard a x) → *

In the logic, we define this function as remove-equal and we leave it enabled. You should never reason about it directly; reason about remove-equal instead.

Definitions and Theorems

Function: remove-equal-without-guard

(defun remove-equal-without-guard (a x)
 (declare (xargs :guard t))
 (let ((__function__ 'remove-equal-without-guard))
  (declare (ignorable __function__))
  (mbe
   :logic (remove-equal a x)
   :exec (cond ((atom x) nil)
               ((equal a (car x))
                (remove-equal-without-guard a (cdr x)))
               (t (cons (car x)
                        (remove-equal-without-guard a (cdr x))))))))