		Search-engine friendly clone of the ACL2 documentation.

Glmc-fsm-p

Change-glmc-fsm

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

Syntax:

(change-glmc-fsm x 
                 [:nextst <nextst>] 
                 [:prop <prop>] 
                 [:fsm-constr <fsm-constr>] 
                 [:bit-constr <bit-constr>] 
                 [:initst <initst>] 
                 [:st-hyp <st-hyp>] 
                 [:hyp <hyp>] 
                 [:st-hyp-next <st-hyp-next>] 
                 [:interp-clauses <interp-clauses>] 
                 [:hyp-var-bound <hyp-var-bound>] 
                 [:var-bound <var-bound>])

This is a sometimes useful alternative to make-glmc-fsm. It constructs a new glmc-fsm-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-fsm

(defmacro change-glmc-fsm (x &rest args)
  (std::change-aggregate
       'glmc-fsm
       x args
       '((:nextst . glmc-fsm->nextst)
         (:prop . glmc-fsm->prop)
         (:fsm-constr . glmc-fsm->fsm-constr)
         (:bit-constr . glmc-fsm->bit-constr)
         (:initst . glmc-fsm->initst)
         (:st-hyp . glmc-fsm->st-hyp)
         (:hyp . glmc-fsm->hyp)
         (:st-hyp-next . glmc-fsm->st-hyp-next)
         (:interp-clauses . glmc-fsm->interp-clauses)
         (:hyp-var-bound . glmc-fsm->hyp-var-bound)
         (:var-bound . glmc-fsm->var-bound))
       'change-glmc-fsm
       'nil))