		Search-engine friendly clone of the ACL2 documentation.

Message

Messagep

Recognizer for message structures.

Signature
(messagep x) → *

Definitions and Theorems

Function: messagep

(defun messagep (x)
 (declare (xargs :guard t))
 (let ((__function__ 'messagep))
  (declare (ignorable __function__))
  (and
    (mbe :logic (and (alistp x)
                     (equal (strip-cars x)
                            '(certificate destination)))
         :exec (fty::alist-with-carsp x '(certificate destination)))
    (b* ((certificate (cdr (std::da-nth 0 x)))
         (destination (cdr (std::da-nth 1 x))))
      (and (certificatep certificate)
           (addressp destination))))))

Theorem: consp-when-messagep

(defthm consp-when-messagep
  (implies (messagep x) (consp x))
  :rule-classes :compound-recognizer)