		Search-engine friendly clone of the ACL2 documentation.

Def-error-checker-implementation

Def-error-checker-bindings

Generate the b* bindings of the error checking function.

Signature
(def-error-checker-bindings conditions-messages error-erp error-val) → bindings
Arguments: conditions-messages — Guard (true-list-listp conditions-messages).; error-erp — The error-erp formal.
Guard (symbolp error-erp).; error-val — The error-val formal.
Guard (symbolp error-val).
Returns: bindings — Type (true-list-listp bindings).

These are the

((unless <conditionj>) (er-soft+ ctx error-erp error-val . <messagej>))

bindings, but a binder of the form (unless (not <condition>)) is turned into (when <condition>) to improve readability.

Definitions and Theorems

Function: def-error-checker-bindings

(defun def-error-checker-bindings
       (conditions-messages error-erp error-val)
 (declare (xargs :guard (and (true-list-listp conditions-messages)
                             (symbolp error-erp)
                             (symbolp error-val))))
 (let ((__function__ 'def-error-checker-bindings))
  (declare (ignorable __function__))
  (b*
   (((when (endp conditions-messages)) nil)
    (condition-message (car conditions-messages))
    (condition (car condition-message))
    (message (cdr condition-message))
    ((mv unless/when condition)
     (case-match condition
       (('not negated-condition)
        (mv 'when negated-condition))
       (& (mv 'unless condition))))
    (binding
     (cons
       (cons unless/when (cons condition 'nil))
       (cons (cons 'er-soft+
                   (cons 'ctx
                         (cons error-erp (cons error-val message))))
             'nil)))
    (bindings (def-error-checker-bindings (cdr conditions-messages)
                                          error-erp error-val)))
   (cons binding bindings))))

Theorem: true-list-listp-of-def-error-checker-bindings

(defthm true-list-listp-of-def-error-checker-bindings
  (b* ((bindings (def-error-checker-bindings conditions-messages
                                             error-erp error-val)))
    (true-list-listp bindings))
  :rule-classes :rewrite)