		Search-engine friendly clone of the ACL2 documentation.

Scratchobj-formals

Change-scratchobj-formals

Modifying constructor for scratchobj-formals structures.

Syntax

(change-scratchobj-formals x 
                           [:val <val>])

This is an often useful alternative to make-scratchobj-formals.

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

(defmacro change-scratchobj-formals (x &rest args)
  (std::change-aggregate 'scratchobj-formals
                         x
                         args '((:val . scratchobj-formals->val))
                         'change-scratchobj-formals
                         'remake-scratchobj-formals))