		Search-engine friendly clone of the ACL2 documentation.

Constant-propagation

Const-prop-transunit

Signature
(const-prop-transunit tunit) → new-tunit
Arguments: tunit — Guard (transunitp tunit).
Returns: new-tunit — Type (transunitp new-tunit).

Definitions and Theorems

Function: const-prop-transunit

(defun const-prop-transunit (tunit)
 (declare (xargs :guard (transunitp tunit)))
 (let ((__function__ 'const-prop-transunit))
  (declare (ignorable __function__))
  (b* (((transunit tunit) tunit))
    (make-transunit :decls (const-prop-extdecl-list tunit.decls nil)
                    :info tunit.info))))

Theorem: transunitp-of-const-prop-transunit

(defthm transunitp-of-const-prop-transunit
  (b* ((new-tunit (const-prop-transunit tunit)))
    (transunitp new-tunit))
  :rule-classes :rewrite)