Restore mv calls in a translated function body.
(atj-restore-mv-calls-in-body body out-types wrld) → new-body
This is the top-level call of atj-restore-mv-calls-in-term:
see that function for details.
We initialize
Function:
(defun atj-restore-mv-calls-in-body (body out-types wrld) (declare (xargs :guard (and (pseudo-termp body) (atj-type-listp out-types) (plist-worldp wrld)))) (let ((__function__ 'atj-restore-mv-calls-in-body)) (declare (ignorable __function__)) (b* ((numres (len out-types)) ((unless (> numres 0)) (raise "Internal error: no output types."))) (atj-restore-mv-calls-in-term body (len out-types) wrld))))
Theorem:
(defthm pseudo-termp-of-atj-restore-mv-calls-in-body (implies (pseudo-termp body) (b* ((new-body (atj-restore-mv-calls-in-body body out-types wrld))) (pseudo-termp new-body))) :rule-classes :rewrite)