		Search-engine friendly clone of the ACL2 documentation.

Error-checking

Ensure-function/lambda-arity

Cause an error if a function or lambda expression does not have a given arity.

Signature
(ensure-function/lambda-arity stobjs-in n description error-erp error-val ctx state) → (mv erp val state)
Arguments: stobjs-in — stobjs-in list of the function or lambda expression whose arity is to be checked.
Guard (symbol-listp stobjs-in).; n — Arity that the function or lambda expression must have.
Guard (natp 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 arity of the function or lambda expression is checked by examining the stobjs-in list of the function or lambda expression. This error-checking function is useful after calling ensure-function/macro/lambda (which returns the stobjs-in list) to handle functions and lambda expressions uniformly. The description parameter should describe the function or lambda expression.

Definitions and Theorems

Function: ensure-function/lambda-arity

(defun ensure-function/lambda-arity
       (stobjs-in n description
                  error-erp error-val ctx state)
  (declare (xargs :stobjs (state)))
  (declare (xargs :guard (and (symbol-listp stobjs-in)
                              (natp n)
                              (msgp description))))
  (b* (((unless (= (len stobjs-in) n))
        (er-soft+ ctx error-erp error-val
                  "~@0 must take ~x1 ~@2." description
                  n (if (= n 1) "argument" "arguments"))))
    (value nil)))

Theorem: return-type-of-ensure-function/lambda-arity.erp

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

Theorem: return-type-of-ensure-function/lambda-arity.val

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