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