		Search-engine friendly clone of the ACL2 documentation.

Processed-stv-p

Change-processed-stv

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

Syntax:

(change-processed-stv x 
                      [:name <name>] 
                      [:user-stv <user-stv>] 
                      [:compiled-stv <compiled-stv>] 
                      [:relevant-signals <relevant-signals>])

This is a sometimes useful alternative to make-processed-stv. It constructs a new processed-stv-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-processed-stv

(defmacro change-processed-stv (x &rest args)
  (std::change-aggregate
       'processed-stv
       x args
       '((:name . processed-stv->name)
         (:user-stv . processed-stv->user-stv)
         (:compiled-stv . processed-stv->compiled-stv)
         (:relevant-signals . processed-stv->relevant-signals))
       'change-processed-stv
       'nil))