|
|
|---|
|
|
|
|---|
Constructor macro for honsed wcp-witness-rule-p structures.
Syntax:
(make-honsed-wcp-witness-rule [:name <name>]
[:enabledp <enabledp>]
[:term <term>]
[:expr <expr>]
[:restriction <restriction>]
[:theorem <theorem>]
[:generalize <generalize>])
This is identical to make-wcp-witness-rule, except that we hons the structure we are creating.
This is an ordinary honsing
Macro:
(defmacro make-honsed-wcp-witness-rule (&rest args) (std::make-aggregate 'wcp-witness-rule args '((:name) (:enabledp) (:term) (:expr) (:restriction) (:theorem) (:generalize)) 'make-honsed-wcp-witness-rule t))