		Search-engine friendly clone of the ACL2 documentation.

Constant-propagation

Const-prop-transunit-ensemble

Transform a translation unit ensemble.

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

Definitions and Theorems

Function: const-prop-transunit-ensemble

(defun const-prop-transunit-ensemble (tunits)
  (declare (xargs :guard (transunit-ensemblep tunits)))
  (let ((__function__ 'const-prop-transunit-ensemble))
    (declare (ignorable __function__))
    (b* (((transunit-ensemble tunits) tunits))
      (transunit-ensemble
           (const-prop-filepath-transunit-map tunits.unwrap)))))

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

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