Restore or calls in a translated term.
(atj-restore-or-calls-in-term term) → new-term
Recall that, at this point, terms have already been type-annotated. Thus, we must take the type annotations into account here, as we recognize and transform the terms.
In general, the test of an if
may be type-annotated differently from its branches,
even when the unannotated test is the same as a branch.
The reason is that the type annotation step ensures that
the branches have the same type
(by inserting suitable type conversions).
Thus, even though an untranslated
When the unwrapped test is equal to the unwrapped `then' branch,
we generate the annotated
Theorem:
(defthm return-type-of-atj-restore-or-calls-in-term.new-term (b* ((?new-term (atj-restore-or-calls-in-term term))) (pseudo-termp new-term)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-atj-restore-or-calls-in-terms.new-terms (b* ((?new-terms (atj-restore-or-calls-in-terms terms))) (pseudo-term-listp new-terms)) :rule-classes :rewrite)
Theorem:
(defthm len-of-atj-restore-or-calls-in-terms (b* ((?new-terms (atj-restore-or-calls-in-terms terms))) (equal (len new-terms) (len terms))))