		Search-engine friendly clone of the ACL2 documentation.

Pinst-keypair

Change-pinst-keypair

Modifying constructor for pinst-keypair structures.

Syntax

(change-pinst-keypair x 
                      [:width <width>] 
                      [:kwd <kwd>] 
                      [:value <value>])

This is an often useful alternative to make-pinst-keypair.

We construct a new pinst-keypair 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-pinst-keypair

(defmacro change-pinst-keypair (x &rest args)
  (std::change-aggregate 'pinst-keypair
                         x args
                         '((:width . pinst-keypair->width)
                           (:kwd . pinst-keypair->kwd)
                           (:value . pinst-keypair->value))
                         'change-pinst-keypair
                         'remake-pinst-keypair))