		Search-engine friendly clone of the ACL2 documentation.

Pinst-special-term

Change-pinst-special-term

Modifying constructor for pinst-special-term structures.

Syntax

(change-pinst-special-term x 
                           [:width <width>] 
                           [:first <first>] 
                           [:init-args-indent <init-args-indent>] 
                           [:init-args <init-args>] 
                           [:body-args-indent <body-args-indent>] 
                           [:body-args <body-args>])

This is an often useful alternative to make-pinst-special-term.

We construct a new pinst-special-term 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 fty::defprod.

Macro: change-pinst-special-term

(defmacro change-pinst-special-term (x &rest args)
  (std::change-aggregate
       'pinst-special-term
       x args
       '((:width . pinst-special-term->width)
         (:first . pinst-special-term->first)
         (:init-args-indent . pinst-special-term->init-args-indent)
         (:init-args . pinst-special-term->init-args)
         (:body-args-indent . pinst-special-term->body-args-indent)
         (:body-args . pinst-special-term->body-args))
       'change-pinst-special-term
       'remake-pinst-special-term))