		Search-engine friendly clone of the ACL2 documentation.

Ctrex-rule

Change-ctrex-rule

Modifying constructor for ctrex-rule structures.

Syntax

(change-ctrex-rule x 
                   [:name <name>] 
                   [:assigned-var <assigned-var>] 
                   [:assign <assign>] 
                   [:match <match>] 
                   [:match-conds <match-conds>] 
                   [:assign-cond <assign-cond>] 
                   [:hyp <hyp>] 
                   [:equiv <equiv>] 
                   [:ruletype <ruletype>])

This is an often useful alternative to make-ctrex-rule.

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

(defmacro change-ctrex-rule (x &rest args)
 (std::change-aggregate 'ctrex-rule
                        x args
                        '((:name . ctrex-rule->name)
                          (:assigned-var . ctrex-rule->assigned-var)
                          (:assign . ctrex-rule->assign)
                          (:match . ctrex-rule->match)
                          (:match-conds . ctrex-rule->match-conds)
                          (:assign-cond . ctrex-rule->assign-cond)
                          (:hyp . ctrex-rule->hyp)
                          (:equiv . ctrex-rule->equiv)
                          (:ruletype . ctrex-rule->ruletype))
                        'change-ctrex-rule
                        'remake-ctrex-rule))