		Search-engine friendly clone of the ACL2 documentation.

Change-gin

Modifying constructor for gin structures.

Syntax

(change-gin x 
            [:ienv <ienv>] 
            [:const-new <const-new>] 
            [:vartys <vartys>] 
            [:events <events>] 
            [:thm-index <thm-index>])

This is an often useful alternative to make-gin.

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

(defmacro change-gin (x &rest args)
  (std::change-aggregate 'gin
                         x args
                         '((:ienv . gin->ienv)
                           (:const-new . gin->const-new)
                           (:vartys . gin->vartys)
                           (:events . gin->events)
                           (:thm-index . gin->thm-index))
                         'change-gin
                         'nil))