		Search-engine friendly clone of the ACL2 documentation.

Transactionp

Transaction

Raw constructor for transactionp structures.

Syntax:

(transaction nonce gas-price gas-limit 
             to value sig-v sig-r sig-s init-or-data)

This is the lowest-level constructor for transactionp structures. It simply conses together a structure with the specified fields.

Note: It's generally better to use macros like make-transaction or change-transaction instead. These macros lead to more readable and robust code, because you don't have to remember the order of the fields.

The transactionp structures we create here are just constructed with ordinary cons. If you want to create honsed structures, see honsed-transaction instead.

Definition

This is an ordinary constructor function introduced by std::defaggregate.

Function: transaction

(defun transaction (nonce gas-price gas-limit
                          to value sig-v sig-r sig-s init-or-data)
 (declare (xargs :guard (and (noncep nonce)
                             (weip gas-price)
                             (n256p gas-limit)
                             (maybe-addressp to)
                             (weip value)
                             (n256p sig-r)
                             (n256p sig-s)
                             (byte-arrayp init-or-data))))
 (cons
  (cons 'nonce nonce)
  (cons
   (cons 'gas-price gas-price)
   (cons
    (cons 'gas-limit gas-limit)
    (cons
     (cons 'to to)
     (cons (cons 'value value)
           (cons (cons 'sig-v sig-v)
                 (cons (cons 'sig-r sig-r)
                       (cons (cons 'sig-s sig-s)
                             (cons (cons 'init-or-data init-or-data)
                                   nil))))))))))