		Search-engine friendly clone of the ACL2 documentation.

Statassert

Statassert->message

Get the message field from a statassert.

Signature
(statassert->message x) → message
Arguments: x — Guard (statassertp x).
Returns: message — Type (stringlit-listp message).

This is an ordinary field accessor created by fty::defprod.

Definitions and Theorems

Function: statassert->message$inline

(defun statassert->message$inline (x)
  (declare (xargs :guard (statassertp x)))
  (declare (xargs :guard t))
  (mbe :logic
       (b* ((x (and t x)))
         (stringlit-list-fix (cdr x)))
       :exec (cdr x)))

Theorem: stringlit-listp-of-statassert->message

(defthm stringlit-listp-of-statassert->message
  (b* ((message (statassert->message$inline x)))
    (stringlit-listp message))
  :rule-classes :rewrite)

Theorem: statassert->message$inline-of-statassert-fix-x

(defthm statassert->message$inline-of-statassert-fix-x
  (equal (statassert->message$inline (statassert-fix x))
         (statassert->message$inline x)))

Theorem: statassert->message$inline-statassert-equiv-congruence-on-x

(defthm statassert->message$inline-statassert-equiv-congruence-on-x
  (implies (statassert-equiv x x-equiv)
           (equal (statassert->message$inline x)
                  (statassert->message$inline x-equiv)))
  :rule-classes :congruence)