		Search-engine friendly clone of the ACL2 documentation.

Ex-from-rp

Context-from-rp

Expands a given context list with the side-conditions from the term

Signature
(context-from-rp term context) → *

Definitions and Theorems

Function: context-from-rp

(defun context-from-rp (term context)
  (declare (xargs :guard t))
  (let ((__function__ 'context-from-rp))
    (declare (ignorable __function__))
    (if (is-rp term)
        (let ((type (car (cdr (car (cdr term)))))
              (x (car (cdr (cdr term)))))
          (b* ((rcontext (context-from-rp x context)))
            (cons (cons type (cons (ex-from-rp x) 'nil))
                  rcontext)))
      context)))