		Search-engine friendly clone of the ACL2 documentation.

Svtv-precompose-data

Change-svtv-precompose-data

Modifying constructor for svtv-precompose-data structures.

Syntax

(change-svtv-precompose-data x 
                             [:simp <simp>] 
                             [:nextstate <nextstate>] 
                             [:input-substs <input-substs>] 
                             [:initst <initst>] 
                             [:pre-compose-inputs <pre-compose-inputs>])

This is an often useful alternative to make-svtv-precompose-data.

We construct a new svtv-precompose-data 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-svtv-precompose-data

(defmacro change-svtv-precompose-data (x &rest args)
 (std::change-aggregate
   'svtv-precompose-data
   x args
   '((:simp . svtv-precompose-data->simp)
     (:nextstate . svtv-precompose-data->nextstate)
     (:input-substs . svtv-precompose-data->input-substs)
     (:initst . svtv-precompose-data->initst)
     (:pre-compose-inputs .
                          svtv-precompose-data->pre-compose-inputs))
   'change-svtv-precompose-data
   'remake-svtv-precompose-data))