Generate the b* bindings of the error checking function.
(def-error-checker-bindings conditions-messages error-erp error-val) → bindings
These are the
((unless <conditionj>) (er-soft+ ctx error-erp error-val . <messagej>))
bindings,
but a binder of the form
Function:
(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:
(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)