		Search-engine friendly clone of the ACL2 documentation.

Rlp-error-fewer-bytes-than-long-length

Change-rlp-error-fewer-bytes-than-long-length

Modifying constructor for rlp-error-fewer-bytes-than-long-length structures.

Syntax

(change-rlp-error-fewer-bytes-than-long-length x 
                                               [:fragment <fragment>] 
                                               [:required <required>] 
                                               [:available <available>])

This is an often useful alternative to make-rlp-error-fewer-bytes-than-long-length.

We construct a new rlp-error-fewer-bytes-than-long-length structure that is a copy of x, except that you can explicitly change some particular fields. Any fields you don't mention just keep their values from x.

Definition

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

Macro: change-rlp-error-fewer-bytes-than-long-length

(defmacro change-rlp-error-fewer-bytes-than-long-length
          (x &rest args)
 (std::change-aggregate
   'rlp-error-fewer-bytes-than-long-length
   x args
   '((:fragment .
                rlp-error-fewer-bytes-than-long-length->fragment)
     (:required .
                rlp-error-fewer-bytes-than-long-length->required)
     (:available .
                 rlp-error-fewer-bytes-than-long-length->available))
   'change-rlp-error-fewer-bytes-than-long-length
   'nil))