		Search-engine friendly clone of the ACL2 documentation.

Svjumpstate

Change-svjumpstate

Modifying constructor for svjumpstate structures.

Syntax

(change-svjumpstate x 
                    [:constraints <constraints>] 
                    [:breakcond <breakcond>] 
                    [:breakst <breakst>] 
                    [:continuecond <continuecond>] 
                    [:continuest <continuest>] 
                    [:returncond <returncond>] 
                    [:returnst <returnst>])

This is an often useful alternative to make-svjumpstate.

We construct a new svjumpstate 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 defprod.

Macro: change-svjumpstate

(defmacro change-svjumpstate (x &rest args)
  (std::change-aggregate
       'svjumpstate
       x args
       '((:constraints . svjumpstate->constraints)
         (:breakcond . svjumpstate->breakcond)
         (:breakst . svjumpstate->breakst)
         (:continuecond . svjumpstate->continuecond)
         (:continuest . svjumpstate->continuest)
         (:returncond . svjumpstate->returncond)
         (:returnst . svjumpstate->returnst))
       'change-svjumpstate
       'nil))