		Search-engine friendly clone of the ACL2 documentation.

Error-checking

Ensure-value-is-untranslated-term

Cause an error if a value is not a term.

Signature
(ensure-value-is-untranslated-term x description error-erp error-val ctx state) → (mv erp val state)
Arguments: x — Value to check.; description — Description of x, for the error messages.
Guard (msgp description).; error-erp — Flag to return in case of error.
Guard (not (null error-erp)).; error-val — Value to return in case of error.; ctx — Context for errors.
Returns: erp — nil or error-erp.; val — A tuple (term stobjs-out) consisting of a pseudo-termp and a symbol-listp if erp is nil; otherwise error-val.

If successful, return the translation of x and the stobjs-out list returned by check-user-term.

If check-user-term fails, the error message it returns is incorporated into a larger error message. Since the message returned by check-user-term starts with the term, it can be incorporated into the larger message without capitalization concerns.

Definitions and Theorems

Function: ensure-value-is-untranslated-term

(defun ensure-value-is-untranslated-term
       (x description
          error-erp error-val ctx state)
  (declare (xargs :stobjs (state)))
  (declare (xargs :guard (and (msgp description)
                              (not (null error-erp)))))
  (let ((__function__ 'ensure-value-is-untranslated-term))
    (declare (ignorable __function__))
    (b* (((mv term/msg stobjs-out)
          (check-user-term x (w state))))
      (if (msgp term/msg)
          (er-soft+ ctx error-erp error-val
                    "~@0 must be an untranslated term.  ~@1"
                    description term/msg)
        (value (list term/msg stobjs-out))))))

Subtopics

Ensure-value-is-untranslated-term$: Call ensure-value-is-untranslated-term with ctx and state as the last two arguments.