		Search-engine friendly clone of the ACL2 documentation.

Inst

Change-inst

Modifying constructor for inst structures.

Syntax

(change-inst x 
             [:mnemonic <mnemonic>] 
             [:opcode <opcode>] 
             [:operands <operands>] 
             [:fn <fn>] 
             [:excep <excep>])

This is an often useful alternative to make-inst.

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

(defmacro change-inst (x &rest args)
  (std::change-aggregate 'inst
                         x args
                         '((:mnemonic . inst->mnemonic)
                           (:opcode . inst->opcode)
                           (:operands . inst->operands)
                           (:fn . inst->fn)
                           (:excep . inst->excep))
                         'change-inst
                         'remake-inst))