		Search-engine friendly clone of the ACL2 documentation.

Module

Change-module

Modifying constructor for module structures.

Syntax

(change-module x 
               [:wires <wires>] 
               [:insts <insts>] 
               [:assigns <assigns>] 
               [:fixups <fixups>] 
               [:constraints <constraints>] 
               [:aliaspairs <aliaspairs>])

This is an often useful alternative to make-module.

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

(defmacro change-module (x &rest args)
  (std::change-aggregate 'module
                         x args
                         '((:wires . module->wires)
                           (:insts . module->insts)
                           (:assigns . module->assigns)
                           (:fixups . module->fixups)
                           (:constraints . module->constraints)
                           (:aliaspairs . module->aliaspairs))
                         'change-module
                         'nil))