		Search-engine friendly clone of the ACL2 documentation.

Error-checking

Ensure-function/lambda/term-number-of-results

Cause an error if a function or lambda expression or term does not have a given number of results.

Signature
(ensure-function/lambda/term-number-of-results stobjs-out n description error-erp error-val ctx state) → (mv erp val state)
Arguments: stobjs-out — stobjs-out list of the function or lambda expression or term whose number of results is to be checked.
Guard (symbol-listp stobjs-out).; n — Number of results that the function or lambda expression or term must have.
Guard (posp n).; 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))) .

The number of results of the function or lambda expression or term is checked by examining the stobjs-out list of the function or lambda expression or term. This error-checking function is useful after calling ensure-function/macro/lambda (for a function or lambda expression) or ensure-value-is-untranslated-term (for a term), both of which return the stobjs-out list, to handle functions and lambda expressions and terms uniformly. The description parameter should describe the function or lambda expression or term.

Definitions and Theorems

Function: ensure-function/lambda/term-number-of-results

(defun ensure-function/lambda/term-number-of-results
       (stobjs-out n description
                   error-erp error-val ctx state)
       (declare (xargs :stobjs (state)))
       (declare (xargs :guard (and (symbol-listp stobjs-out)
                                   (posp n)
                                   (msgp description))))
       (b* (((unless (= (len stobjs-out) n))
             (er-soft+ ctx error-erp error-val
                       "~@0 must return ~x1 ~@2." description
                       n (if (= n 1) "result" "results"))))
           (value nil)))

Theorem: return-type-of-ensure-function/lambda/term-number-of-results.erp

(defthm
    return-type-of-ensure-function/lambda/term-number-of-results.erp
    (b* (((mv ?erp ?val ?state)
          (ensure-function/lambda/term-number-of-results
               stobjs-out n description
               error-erp error-val ctx state)))
        (implies erp (equal erp error-erp)))
    :rule-classes :rewrite)

Theorem: return-type-of-ensure-function/lambda/term-number-of-results.val

(defthm
    return-type-of-ensure-function/lambda/term-number-of-results.val
    (b* (((mv ?erp ?val ?state)
          (ensure-function/lambda/term-number-of-results
               stobjs-out n 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-function/lambda/term-number-of-results$: Calls ensure-function/lambda/term-number-of-results with ctx and state as the last two arguments.