Top

Rp-utilities

Ex-from-rp

Extracts a term if it is wrapped in an rp instance.

Signature
(ex-from-rp term) → *

Definitions and Theorems

Function: ex-from-rp

(defun ex-from-rp (term)
  (declare (xargs :guard t))
  (let ((__function__ 'ex-from-rp))
    (declare (ignorable __function__))
    (if (is-rp term)
        (ex-from-rp (caddr term))
      term)))

Subtopics

Context-from-rp: Expands a given context list with the side-conditions from the term
Ex-from-rp-loose: Same as ex-from-rp when term is rp-termp but a little faster.
Ex-from-rp-all2: Removes all instances of 'rp' from a term, and remove falist instances along the way
Ex-from-rp-all: Removes all instances of 'rp' from a term