		Search-engine friendly clone of the ACL2 documentation.

Specialize-implementation

Specialize-transunit-ensemble

Transform a translation unit ensemble.

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

Definitions and Theorems

Function: specialize-transunit-ensemble

(defun specialize-transunit-ensemble
       (tunits target-fn target-param const)
  (declare (xargs :guard (and (transunit-ensemblep tunits)
                              (identp target-fn)
                              (identp target-param)
                              (exprp const))))
  (b* (((transunit-ensemble tunits) tunits))
    (transunit-ensemble (specialize-filepath-transunit-map
                             tunits.unwrap
                             target-fn target-param const))))

Theorem: transunit-ensemblep-of-specialize-transunit-ensemble

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