		Search-engine friendly clone of the ACL2 documentation.

Message-endorsement

Make-message-endorsement

Basic constructor macro for message-endorsement structures.

Syntax

(make-message-endorsement [:proposal <proposal>] 
                          [:endorser <endorser>])

This is the usual way to construct message-endorsement structures. It simply conses together a structure with the specified fields.

This macro generates a new message-endorsement structure from scratch. See also change-message-endorsement, which can "change" an existing structure, instead.

Definition

This is an ordinary make- macro introduced by fty::defprod.

Macro: make-message-endorsement

(defmacro make-message-endorsement (&rest args)
  (std::make-aggregate 'message-endorsement
                       args '((:proposal) (:endorser))
                       'make-message-endorsement
                       nil))

Function: message-endorsement

(defun message-endorsement (proposal endorser)
  (declare (xargs :guard (and (proposalp proposal)
                              (addressp endorser))))
  (declare (xargs :guard t))
  (let ((__function__ 'message-endorsement))
    (declare (ignorable __function__))
    (b* ((proposal (mbe :logic (proposal-fix proposal)
                        :exec proposal))
         (endorser (mbe :logic (address-fix endorser)
                        :exec endorser)))
      (cons :endorsement (list proposal endorser)))))