		Search-engine friendly clone of the ACL2 documentation.

Atj-pre-translation-remove-return-last

Atj-remove-return-last

Remove all the return-lasts from a term.

Signature
(atj-remove-return-last term guards$) → new-term
Arguments: term — Guard (pseudo-termp term).; guards$ — Guard (booleanp guards$).
Returns: new-term — Type (pseudo-termp new-term), given (pseudo-termp term).

Definitions and Theorems

Function: atj-remove-return-last

(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: pseudo-termp-of-atj-remove-return-last

(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)