|
|
|---|
|
|
|
|---|
Constructor macro for wcp-witness-rule-p structures.
Syntax:
(make-wcp-witness-rule [:name <name>]
[:enabledp <enabledp>]
[:term <term>]
[:expr <expr>]
[:restriction <restriction>]
[:theorem <theorem>]
[:generalize <generalize>])
This is our preferred way to construct wcp-witness-rule-p structures. It simply conses together a structure with the specified fields.
This macro generates a new wcp-witness-rule-p structure from scratch. See also change-wcp-witness-rule, which can "change" an existing structure, instead.
The wcp-witness-rule-p structures we create here are just constructed with ordinary cons. If you want to create honsed structures, see make-honsed-wcp-witness-rule instead.
This is an ordinary
Macro:
(defmacro make-wcp-witness-rule (&rest args) (std::make-aggregate 'wcp-witness-rule args '((:name) (:enabledp) (:term) (:expr) (:restriction) (:theorem) (:generalize)) 'make-wcp-witness-rule nil))