		Search-engine friendly clone of the ACL2 documentation.

Bit-blasting

Symbolic-params-x-out-cond

Signature
(symbolic-params-x-out-cond symbolic-params) → *
Arguments: symbolic-params — Guard (alistp symbolic-params).

Definitions and Theorems

Function: symbolic-params-x-out-cond

(defun symbolic-params-x-out-cond (symbolic-params)
  (declare (xargs :guard (alistp symbolic-params)))
  (let ((__function__ 'symbolic-params-x-out-cond))
    (declare (ignorable __function__))
    (and (cdr (assoc :simplify symbolic-params))
         (not (cdr (assoc :all-vars symbolic-params))))))