		Search-engine friendly clone of the ACL2 documentation.

Smt-solver-params

Smt-solver-params-fix

Fixing function for smt-solver-params.

Signature
(smt-solver-params-fix term) → fixed-term
Arguments: term — Guard (smt-solver-params-p term).
Returns: fixed-term — Type (smt-solver-params-p fixed-term).

Definitions and Theorems

Function: smt-solver-params-fix

(defun smt-solver-params-fix (term)
  (declare (xargs :guard (smt-solver-params-p term)))
  (let ((acl2::__function__ 'smt-solver-params-fix))
    (declare (ignorable acl2::__function__))
    (mbe :logic
         (if (smt-solver-params-p term)
             term
           (true-list-fix term))
         :exec term)))

Theorem: smt-solver-params-p-of-smt-solver-params-fix

(defthm smt-solver-params-p-of-smt-solver-params-fix
  (b* ((fixed-term (smt-solver-params-fix term)))
    (smt-solver-params-p fixed-term))
  :rule-classes :rewrite)