		Search-engine friendly clone of the ACL2 documentation.

Errors

Error-info-wfp

Check if the information in an error is well-formed.

Signature
(error-info-wfp error) → yes/no
Arguments: error — Guard (reserrp error).
Returns: yes/no — Type (booleanp yes/no).

For certain purposes, we need to know that the errors generated (and propagated) in our Yul formalization are well-formed according to certain criteria. Specifically, we need to know that the information is always a cons. For better encapsulation and possible future extension, we capture that in this predicate.

Definitions and Theorems

Function: error-info-wfp

(defun error-info-wfp (error)
  (declare (xargs :guard (reserrp error)))
  (let ((__function__ 'error-info-wfp))
    (declare (ignorable __function__))
    (consp (fty::reserr->info error))))

Theorem: booleanp-of-error-info-wfp

(defthm booleanp-of-error-info-wfp
  (b* ((yes/no (error-info-wfp error)))
    (booleanp yes/no))
  :rule-classes :rewrite)

Theorem: error-info-wfp-of-reserr-of-cons

(defthm error-info-wfp-of-reserr-of-cons
  (error-info-wfp (reserr (cons a b))))

Theorem: error-info-wfp-of-reserr-fix-error

(defthm error-info-wfp-of-reserr-fix-error
  (equal (error-info-wfp (fty::reserr-fix error))
         (error-info-wfp error)))

Theorem: error-info-wfp-reserr-equiv-congruence-on-error

(defthm error-info-wfp-reserr-equiv-congruence-on-error
  (implies (fty::reserr-equiv error error-equiv)
           (equal (error-info-wfp error)
                  (error-info-wfp error-equiv)))
  :rule-classes :congruence)