		Search-engine friendly clone of the ACL2 documentation.

Glmc-config-p

Change-glmc-config

A copying macro that lets you create new glmc-config-p structures, based on existing structures.

Syntax:

(change-glmc-config x 
                    [:glcp-config <glcp-config>] 
                    [:st-var <st-var>] 
                    [:in-vars <in-vars>] 
                    [:frame-ins <frame-ins>] 
                    [:rest-ins <rest-ins>] 
                    [:end-ins <end-ins>] 
                    [:frame-in-vars <frame-in-vars>] 
                    [:in-measure <in-measure>] 
                    [:run <run>] 
                    [:st-hyp <st-hyp>] 
                    [:in-hyp <in-hyp>] 
                    [:bindings <bindings>] 
                    [:bound-vars <bound-vars>] 
                    [:initstp <initstp>] 
                    [:nextst <nextst>] 
                    [:constr <constr>] 
                    [:prop <prop>] 
                    [:st-hyp-method <st-hyp-method>] 
                    [:hints <hints>] 
                    [:main-rewrite-rules <main-rewrite-rules>] 
                    [:main-branch-merge-rules <main-branch-merge-rules>] 
                    [:extract-rewrite-rules <extract-rewrite-rules>] 
                    [:extract-branch-merge-rules <extract-branch-merge-rules>])

This is a sometimes useful alternative to make-glmc-config. It constructs a new glmc-config-p 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 std::defaggregate.

Macro: change-glmc-config

(defmacro change-glmc-config (x &rest args)
 (std::change-aggregate
     'glmc-config
     x args
     '((:glcp-config . glmc-config->glcp-config)
       (:st-var . glmc-config->st-var)
       (:in-vars . glmc-config->in-vars)
       (:frame-ins . glmc-config->frame-ins)
       (:rest-ins . glmc-config->rest-ins)
       (:end-ins . glmc-config->end-ins)
       (:frame-in-vars . glmc-config->frame-in-vars)
       (:in-measure . glmc-config->in-measure)
       (:run . glmc-config->run)
       (:st-hyp . glmc-config->st-hyp)
       (:in-hyp . glmc-config->in-hyp)
       (:bindings . glmc-config->bindings)
       (:bound-vars . glmc-config->bound-vars)
       (:initstp . glmc-config->initstp)
       (:nextst . glmc-config->nextst)
       (:constr . glmc-config->constr)
       (:prop . glmc-config->prop)
       (:st-hyp-method . glmc-config->st-hyp-method)
       (:hints . glmc-config->hints)
       (:main-rewrite-rules . glmc-config->main-rewrite-rules)
       (:main-branch-merge-rules
            . glmc-config->main-branch-merge-rules)
       (:extract-rewrite-rules . glmc-config->extract-rewrite-rules)
       (:extract-branch-merge-rules
            .
            glmc-config->extract-branch-merge-rules))
     'change-glmc-config
     'nil))