		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>] 
                   [:match <match>] 
                   [:unify-subst <unify-subst>] 
                   [:target <target>] 
                   [:deps <deps>] 
                   [:dep-success-vars <dep-success-vars>] 
                   [:success <success>] 
                   [:priority <priority>] 
                   [:value <value>] 
                   [:order <order>] 
                   [: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)
         (:match . ctrex-rule->match)
         (:unify-subst . ctrex-rule->unify-subst)
         (:target . ctrex-rule->target)
         (:deps . ctrex-rule->deps)
         (:dep-success-vars . ctrex-rule->dep-success-vars)
         (:success . ctrex-rule->success)
         (:priority . ctrex-rule->priority)
         (:value . ctrex-rule->value)
         (:order . ctrex-rule->order)
         (:ruletype . ctrex-rule->ruletype))
       'change-ctrex-rule
       'nil))