		Search-engine friendly clone of the ACL2 documentation.

Specialize-implementation

Specialize-transunit

Transform a translation unit.

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

Definitions and Theorems

Function: specialize-transunit

(defun specialize-transunit (tunit target-fn target-param const)
 (declare (xargs :guard (and (transunitp tunit)
                             (identp target-fn)
                             (identp target-param)
                             (exprp const))))
 (b* (((transunit tunit) tunit))
  (make-transunit
       :decls (specialize-extdecl-list tunit.decls
                                       target-fn target-param const)
       :info tunit.info)))

Theorem: transunitp-of-specialize-transunit

(defthm transunitp-of-specialize-transunit
  (b*
   ((new-tunit
         (specialize-transunit tunit target-fn target-param const)))
   (transunitp new-tunit))
  :rule-classes :rewrite)