		Search-engine friendly clone of the ACL2 documentation.

Ex-from-rp

Ex-from-rp-loose

Same as ex-from-rp when term is rp-termp but a little faster.

Signature
(ex-from-rp-loose term) → *

Definitions and Theorems

Function: ex-from-rp-loose

(defun ex-from-rp-loose (term)
  (declare (xargs :guard t))
  (let ((__function__ 'ex-from-rp-loose))
    (declare (ignorable __function__))
    (mbe :logic
         (if (is-rp-loose term)
             (ex-from-rp-loose (caddr term))
           term)
         :exec
         (case-match term
           (('rp & x) (ex-from-rp-loose x))
           (& term)))))