		Search-engine friendly clone of the ACL2 documentation.

Simpadd0-gout

Change-simpadd0-gout

Modifying constructor for simpadd0-gout structures.

Syntax

(change-simpadd0-gout x 
                      [:events <events>] 
                      [:thm-name <thm-name>] 
                      [:thm-index <thm-index>] 
                      [:names-to-avoid <names-to-avoid>] 
                      [:vartys <vartys>] 
                      [:diffp <diffp>])

This is an often useful alternative to make-simpadd0-gout.

We construct a new simpadd0-gout 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-simpadd0-gout

(defmacro change-simpadd0-gout (x &rest args)
  (std::change-aggregate
       'simpadd0-gout
       x args
       '((:events . simpadd0-gout->events)
         (:thm-name . simpadd0-gout->thm-name)
         (:thm-index . simpadd0-gout->thm-index)
         (:names-to-avoid . simpadd0-gout->names-to-avoid)
         (:vartys . simpadd0-gout->vartys)
         (:diffp . simpadd0-gout->diffp))
       'change-simpadd0-gout
       'nil))