|
|
|---|
|
|
|
|---|
Constructor macro for honsed constraint-rule-p structures.
Syntax:
(make-honsed-constraint-rule [:thmname <thmname>]
[:lit-alist <lit-alist>]
[:syntaxp <syntaxp>])
This is identical to make-constraint-rule, except that we hons the structure we are creating.
This is an ordinary honsing
Macro:
(defmacro make-honsed-constraint-rule (&rest args) (std::make-aggregate 'constraint-rule args '((:thmname) (:lit-alist) (:syntaxp)) 'make-honsed-constraint-rule t))