		Search-engine friendly clone of the ACL2 documentation.

Bfr-to-param-space

Bfr-to-param-space-weak

Same as bfr-to-param-space for BDDs, but don't bother to do anything if we're working with AIGs.

Signature
(bfr-to-param-space-weak p x) → *

Definitions and Theorems

Function: bfr-to-param-space-weak

(defun bfr-to-param-space-weak (p x)
  (declare (xargs :guard t))
  (let ((__function__ 'bfr-to-param-space-weak))
    (declare (ignorable __function__))
    (bfr-case :bdd (acl2::to-param-space p x)
              :aig x)))