		Search-engine friendly clone of the ACL2 documentation.

Error-checking

Ensure-boolean-or-auto-and-return-boolean

Cause an error if a value is not t, nil, or :auto; otherwise return a boolean result.

Signature
(ensure-boolean-or-auto-and-return-boolean x r description error-erp error-val ctx state) → (mv erp val state)
Arguments: x — Value to check.; r — Value to return if x is :auto.
Guard (booleanp r).; 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 (booleanp r)) (booleanp val))) .

If x is a boolean, return it as result. If x is :auto, return the boolean r, as if :auto meant copying the result from r.

Definitions and Theorems

Function: ensure-boolean-or-auto-and-return-boolean

(defun ensure-boolean-or-auto-and-return-boolean
       (x r description
          error-erp error-val ctx state)
  (declare (xargs :stobjs (state)))
  (declare (xargs :guard (and (booleanp r) (msgp description))))
  (b* (((unless (t/nil/auto-p x))
        (er-soft+ ctx error-erp error-val
                  "~@0 must be T, NIL, or :AUTO."
                  description)))
    (value (if (booleanp x) x r))))

Theorem: return-type-of-ensure-boolean-or-auto-and-return-boolean.erp

(defthm return-type-of-ensure-boolean-or-auto-and-return-boolean.erp
  (b* (((mv ?erp ?val ?state)
        (ensure-boolean-or-auto-and-return-boolean
             x r description
             error-erp error-val ctx state)))
    (implies erp (equal erp error-erp)))
  :rule-classes :rewrite)

Theorem: return-type-of-ensure-boolean-or-auto-and-return-boolean.val

(defthm return-type-of-ensure-boolean-or-auto-and-return-boolean.val
  (b* (((mv ?erp ?val ?state)
        (ensure-boolean-or-auto-and-return-boolean
             x r description
             error-erp error-val ctx state)))
    (and (implies erp (equal val error-val))
         (implies (and (not erp) error-erp (booleanp r))
                  (booleanp val))))
  :rule-classes :rewrite)

Subtopics

Ensure-boolean-or-auto-and-return-boolean$: Calls ensure-boolean-or-auto-and-return-boolean with ctx and state as the last two arguments.