		Search-engine friendly clone of the ACL2 documentation.

Wcp-instance-rule-p

Change-wcp-instance-rule

A copying macro that lets you create new wcp-instance-rule-p structures, based on existing structures.

Syntax:

(change-wcp-instance-rule x 
                          [:name <name>] 
                          [:enabledp <enabledp>] 
                          [:pred <pred>] 
                          [:vars <vars>] 
                          [:expr <expr>] 
                          [:restriction <restriction>] 
                          [:theorem <theorem>])

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

(defmacro change-wcp-instance-rule (x &rest args)
  (std::change-aggregate
       'wcp-instance-rule
       x args
       '((:name . wcp-instance-rule->name)
         (:enabledp . wcp-instance-rule->enabledp)
         (:pred . wcp-instance-rule->pred)
         (:vars . wcp-instance-rule->vars)
         (:expr . wcp-instance-rule->expr)
         (:restriction . wcp-instance-rule->restriction)
         (:theorem . wcp-instance-rule->theorem))
       'change-wcp-instance-rule
       'nil))