|
|
|---|
|
|
|
|---|
Modifying constructor for simpadd0-gin structures.
(change-simpadd0-gin x
[:thm-index <thm-index>]
[:names-to-avoid <names-to-avoid>])
This is an often useful alternative to make-simpadd0-gin.
We construct a new simpadd0-gin structure that is a copy of
This is an ordinary
Macro:
(defmacro change-simpadd0-gin (x &rest args) (std::change-aggregate 'simpadd0-gin x args '((:thm-index . simpadd0-gin->thm-index) (:names-to-avoid . simpadd0-gin->names-to-avoid)) 'change-simpadd0-gin 'nil))