		Search-engine friendly clone of the ACL2 documentation.

Rp-utilities

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 ((acl2::__function__ 'ex-from-rp-loose))
        (declare (ignorable acl2::__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)))))