		Search-engine friendly clone of the ACL2 documentation.

Specialize-implementation

Specialize-code-ensemble

Transform a code ensemble.

Signature
(specialize-code-ensemble code target-fn target-param const) → new-code
Arguments: code — Guard (code-ensemblep code).; target-fn — Guard (identp target-fn).; target-param — Guard (identp target-param).; const — Guard (exprp const).
Returns: new-code — Type (code-ensemblep new-code).

Definitions and Theorems

Function: specialize-code-ensemble

(defun specialize-code-ensemble (code target-fn target-param const)
 (declare (xargs :guard (and (code-ensemblep code)
                             (identp target-fn)
                             (identp target-param)
                             (exprp const))))
 (b* (((code-ensemble code) code))
   (make-code-ensemble
        :transunits
        (specialize-transunit-ensemble code.transunits
                                       target-fn target-param const)
        :ienv code.ienv)))

Theorem: code-ensemblep-of-specialize-code-ensemble

(defthm code-ensemblep-of-specialize-code-ensemble
 (b*
  ((new-code
      (specialize-code-ensemble code target-fn target-param const)))
  (code-ensemblep new-code))
 :rule-classes :rewrite)