		Search-engine friendly clone of the ACL2 documentation.

Instruction-hash

Change-instruction-hash

Modifying constructor for instruction-hash structures.

Syntax

(change-instruction-hash x 
                         [:op <op>] 
                         [:arg <arg>] 
                         [:into <into>])

This is an often useful alternative to make-instruction-hash.

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

(defmacro change-instruction-hash (x &rest args)
  (std::change-aggregate 'instruction-hash
                         x args
                         '((:op . instruction-hash->op)
                           (:arg . instruction-hash->arg)
                           (:into . instruction-hash->into))
                         'change-instruction-hash
                         'nil))