		Search-engine friendly clone of the ACL2 documentation.

Remove-mbe-logic

Turn every call (mbe :logic a :exec b) in a term into just its :exec part b.

Signature
(remove-mbe-logic term) → new-term
Arguments: term — Guard (pseudo-termp term).
Returns: new-term — Type (pseudo-termp new-term), given the guard.

Definitions and Theorems

Function: remove-mbe-logic

(defun remove-mbe-logic (term)
  (declare (xargs :guard (pseudo-termp term)))
  (let ((__function__ 'remove-mbe-logic))
    (declare (ignorable __function__))
    (remove-mbe-logic/exec term t)))

Theorem: pseudo-termp-of-remove-mbe-logic

(defthm pseudo-termp-of-remove-mbe-logic
  (implies (and (pseudo-termp term))
           (b* ((new-term (remove-mbe-logic term)))
             (pseudo-termp new-term)))
  :rule-classes :rewrite)