		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
           :declons (const-prop-ext-declon-list tunit.declons 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)