		Search-engine friendly clone of the ACL2 documentation.

Proposal

Make-proposal

Basic constructor macro for proposal structures.

Syntax

(make-proposal [:author <author>] 
               [:round <round>] 
               [:transactions <transactions>] 
               [:previous <previous>])

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

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

Definition

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

Macro: make-proposal

(defmacro make-proposal (&rest args)
  (std::make-aggregate 'proposal
                       args
                       '((:author)
                         (:round)
                         (:transactions)
                         (:previous))
                       'make-proposal
                       nil))

Function: proposal

(defun proposal (author round transactions previous)
 (declare (xargs :guard (and (addressp author)
                             (posp round)
                             (transaction-listp transactions)
                             (address-setp previous))))
 (declare (xargs :guard t))
 (let ((__function__ 'proposal))
  (declare (ignorable __function__))
  (b* ((author (mbe :logic (address-fix author)
                    :exec author))
       (round (mbe :logic (pos-fix round)
                   :exec round))
       (transactions (mbe :logic (transaction-list-fix transactions)
                          :exec transactions))
       (previous (mbe :logic (address-set-fix previous)
                      :exec previous)))
    (list (cons 'author author)
          (cons 'round round)
          (cons 'transactions transactions)
          (cons 'previous previous)))))