		Search-engine friendly clone of the ACL2 documentation.

Error-checking

Ensure-term-free-vars-subset

Cause an error if a term includes free variables outside a given set.

Signature
(ensure-term-free-vars-subset term vars description error-erp error-val ctx state) → (mv erp val state)
Arguments: term — Term to check.
Guard (pseudo-termp term).; vars — Variables that must include all the free variables of term.
Guard (symbol-listp vars).; description — Guard (msgp description).; error-erp — Flag to return in case of error.; error-val — Value to return in case of error.; ctx — Context for errors.
Returns: erp — Type (implies erp (equal erp error-erp)).; val — Type (and (implies erp (equal val error-val)) (implies (and (not erp) error-erp) (not val))) .

Definitions and Theorems

Function: ensure-term-free-vars-subset

(defun ensure-term-free-vars-subset
       (term vars description
             error-erp error-val ctx state)
 (declare (xargs :stobjs (state)))
 (declare (xargs :guard (and (pseudo-termp term)
                             (symbol-listp vars)
                             (msgp description))))
 (b*
  (((unless (subsetp-eq (all-vars term) vars))
    (er-soft+
     ctx error-erp error-val
     "~@0 must contain no free variables other than ~&1, ~
     but it contains the ~@2."
     description vars
     (let ((extra (set-difference-eq (all-vars term)
                                     vars)))
       (if (= (len extra) 1)
           (msg "variable ~x0" (car extra))
         (msg "variables ~&0" extra))))))
  (value nil)))

Theorem: return-type-of-ensure-term-free-vars-subset.erp

(defthm return-type-of-ensure-term-free-vars-subset.erp
  (b*
    (((mv ?erp ?val ?state)
      (ensure-term-free-vars-subset term vars description
                                    error-erp error-val ctx state)))
    (implies erp (equal erp error-erp)))
  :rule-classes :rewrite)

Theorem: return-type-of-ensure-term-free-vars-subset.val

(defthm return-type-of-ensure-term-free-vars-subset.val
  (b*
    (((mv ?erp ?val ?state)
      (ensure-term-free-vars-subset term vars description
                                    error-erp error-val ctx state)))
    (and (implies erp (equal val error-val))
         (implies (and (not erp) error-erp)
                  (not val))))
  :rule-classes :rewrite)

Subtopics

Ensure-term-free-vars-subset$: Calls ensure-term-free-vars-subset with ctx and state as the last two arguments.