		Search-engine friendly clone of the ACL2 documentation.

Error-checking

Ensure-function/lambda-logic-mode

Cause an error if a function or lambda expression is a function in program mode or a lambda expression that calls some program-mode function.

Signature
(ensure-function/lambda-logic-mode fn/lambda description error-erp error-val ctx state) → (mv erp val state)
Arguments: fn/lambda — Function or lambda expression to check.
Guard (pseudo-termfnp fn/lambda).; 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))) .

This error-checking function is useful after calling ensure-function/macro/lambda (which returns the pseudo-termfnp) to handle functions and lambda expressions uniformly. The description parameter should describe the function or lambda expression.

Definitions and Theorems

Function: ensure-function/lambda-logic-mode

(defun ensure-function/lambda-logic-mode
       (fn/lambda description
                  error-erp error-val ctx state)
 (declare (xargs :stobjs (state)))
 (declare (xargs :guard (and (pseudo-termfnp fn/lambda)
                             (msgp description))))
 (let ((__function__ 'ensure-function/lambda-logic-mode))
   (declare (ignorable __function__))
   (if
    (symbolp fn/lambda)
    (ensure-function-is-logic-mode$ fn/lambda
                                    description error-erp error-val)
    (ensure-lambda-logic-mode$ fn/lambda
                               description error-erp error-val))))

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

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

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

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