Remove all the return-lasts from a term.
(atj-remove-return-last term guards$) → new-term
Function:
(defun atj-remove-return-last (term guards$) (declare (xargs :guard (and (pseudo-termp term) (booleanp guards$)))) (let ((__function__ 'atj-remove-return-last)) (declare (ignorable __function__)) (b* ((term (if guards$ (remove-mbe-logic term) (remove-mbe-exec term))) (term (remove-progn term))) term)))
Theorem:
(defthm pseudo-termp-of-atj-remove-return-last (implies (pseudo-termp term) (b* ((new-term (atj-remove-return-last term guards$))) (pseudo-termp new-term))) :rule-classes :rewrite)