		Search-engine friendly clone of the ACL2 documentation.

Modscope-nested

Change-modscope-nested

Modifying constructor for modscope-nested structures.

Syntax

(change-modscope-nested x 
                        [:modidx <modidx>] 
                        [:wireoffset <wireoffset>] 
                        [:instoffset <instoffset>] 
                        [:upper <upper>])

This is an often useful alternative to make-modscope-nested.

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

(defmacro change-modscope-nested (x &rest args)
  (std::change-aggregate
       'modscope-nested
       x args
       '((:modidx . modscope-nested->modidx)
         (:wireoffset . modscope-nested->wireoffset)
         (:instoffset . modscope-nested->instoffset)
         (:upper . modscope-nested->upper))
       'change-modscope-nested
       'remake-modscope-nested))