		Search-engine friendly clone of the ACL2 documentation.

Stv-spec-p

Change-stv-spec

A copying macro that lets you create new stv-spec-p structures, based on existing structures.

Syntax:

(change-stv-spec x 
                 [:mod <mod>] 
                 [:inputs <inputs>] 
                 [:outputs <outputs>] 
                 [:internals <internals>] 
                 [:overrides <overrides>])

This is a sometimes useful alternative to make-stv-spec. It constructs a new stv-spec-p 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 std::defaggregate.

Macro: change-stv-spec

(defmacro change-stv-spec (x &rest args)
  (std::change-aggregate 'stv-spec
                         x args
                         '((:mod . stv-spec->mod)
                           (:inputs . stv-spec->inputs)
                           (:outputs . stv-spec->outputs)
                           (:internals . stv-spec->internals)
                           (:overrides . stv-spec->overrides))
                         'change-stv-spec
                         'nil))