		Search-engine friendly clone of the ACL2 documentation.

Simpadd0

Simpadd0-transunit

Transform a translation unit.

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

Definitions and Theorems

Function: simpadd0-transunit

(defun simpadd0-transunit (tunit)
  (declare (xargs :guard (transunitp tunit)))
  (declare (xargs :guard (transunit-unambp tunit)))
  (let ((__function__ 'simpadd0-transunit))
    (declare (ignorable __function__))
    (b* (((transunit tunit) tunit))
      (transunit (simpadd0-extdecl-list tunit.decls)))))

Theorem: transunitp-of-simpadd0-transunit

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

Theorem: transunit-unambp-of-simpadd0-transunit

(defthm transunit-unambp-of-simpadd0-transunit
  (b* ((?new-tunit (simpadd0-transunit tunit)))
    (transunit-unambp new-tunit)))

Theorem: simpadd0-transunit-of-transunit-fix-tunit

(defthm simpadd0-transunit-of-transunit-fix-tunit
  (equal (simpadd0-transunit (c$::transunit-fix tunit))
         (simpadd0-transunit tunit)))

Theorem: simpadd0-transunit-transunit-equiv-congruence-on-tunit

(defthm simpadd0-transunit-transunit-equiv-congruence-on-tunit
  (implies (c$::transunit-equiv tunit tunit-equiv)
           (equal (simpadd0-transunit tunit)
                  (simpadd0-transunit tunit-equiv)))
  :rule-classes :congruence)