		Search-engine friendly clone of the ACL2 documentation.

Error-checking

Ensure-keyword-value-list

Cause an error if a value if not a true list of even length with keywords at its even-numbered positions (counting from 0).

Signature
(ensure-keyword-value-list x description error-erp error-val ctx state) → (mv erp val state)
Arguments: x — Value to check.; 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))) .

Definitions and Theorems

Function: ensure-keyword-value-list

(defun ensure-keyword-value-list (x description
                                    error-erp error-val ctx state)
 (declare (xargs :stobjs (state)))
 (declare (xargs :guard (msgp description)))
 (b*
  (((unless (keyword-value-listp x))
    (er-soft+
     ctx error-erp error-val
     "~@0 must a true list of even length ~
                             with keywords at its even-numbered positions ~
                             (counting from 0)."
     description)))
  (value nil)))

Theorem: return-type-of-ensure-keyword-value-list.erp

(defthm return-type-of-ensure-keyword-value-list.erp
  (b* (((mv ?erp ?val ?state)
        (ensure-keyword-value-list x description
                                   error-erp error-val ctx state)))
    (implies erp (equal erp error-erp)))
  :rule-classes :rewrite)

Theorem: return-type-of-ensure-keyword-value-list.val

(defthm return-type-of-ensure-keyword-value-list.val
  (b* (((mv ?erp ?val ?state)
        (ensure-keyword-value-list x 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-keyword-value-list$: Calls ensure-keyword-value-list with ctx and state as the last two arguments.