		Search-engine friendly clone of the ACL2 documentation.

A4vec

Change-a4vec

Modifying constructor for a4vec structures.

Syntax

(change-a4vec x 
              [:upper <upper>] 
              [:lower <lower>])

This is an often useful alternative to make-a4vec.

We construct a new a4vec 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 defprod.

Macro: change-a4vec

(defmacro change-a4vec (x &rest args)
  (std::change-aggregate 'a4vec
                         x args
                         '((:upper . a4vec->upper)
                           (:lower . a4vec->lower))
                         'change-a4vec
                         'remake-a4vec))