		Search-engine friendly clone of the ACL2 documentation.

Wcp-instance-rule-p

Make-wcp-instance-rule

Constructor macro for wcp-instance-rule-p structures.

Syntax:

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

This is our preferred way to construct wcp-instance-rule-p structures. It simply conses together a structure with the specified fields.

This macro generates a new wcp-instance-rule-p structure from scratch. See also change-wcp-instance-rule, which can "change" an existing structure, instead.

The wcp-instance-rule-p structures we create here are just constructed with ordinary cons. If you want to create honsed structures, see make-honsed-wcp-instance-rule instead.

Definition

This is an ordinary make- macro introduced by std::defaggregate.

Macro: make-wcp-instance-rule

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