		Search-engine friendly clone of the ACL2 documentation.

Constant-propagation

Const-prop-code-ensemble

Transform a code ensemble.

Signature
(const-prop-code-ensemble code) → new-code
Arguments: code — Guard (code-ensemblep code).
Returns: new-code — Type (code-ensemblep new-code).

Definitions and Theorems

Function: const-prop-code-ensemble

(defun const-prop-code-ensemble (code)
 (declare (xargs :guard (code-ensemblep code)))
 (let ((__function__ 'const-prop-code-ensemble))
  (declare (ignorable __function__))
  (b* (((code-ensemble code) code))
    (make-code-ensemble
         :transunits (const-prop-transunit-ensemble code.transunits)
         :ienv code.ienv))))

Theorem: code-ensemblep-of-const-prop-code-ensemble

(defthm code-ensemblep-of-const-prop-code-ensemble
  (b* ((new-code (const-prop-code-ensemble code)))
    (code-ensemblep new-code))
  :rule-classes :rewrite)