|
|
|---|
|
|
|
|---|
Raw constructor for constraint-rule-p structures.
Syntax:
(constraint-rule thmname lit-alist syntaxp)
This is the lowest-level constructor for constraint-rule-p structures. It simply conses together a structure with the specified fields.
Note: It's generally better to use macros like make-constraint-rule or change-constraint-rule instead. These macros lead to more readable and robust code, because you don't have to remember the order of the fields.
The constraint-rule-p structures we create here are just constructed with ordinary cons. If you want to create honsed structures, see honsed-constraint-rule instead.
This is an ordinary constructor function introduced by std::defaggregate.
Function:
(defun constraint-rule (thmname lit-alist syntaxp) (declare (xargs :guard (and))) (cons (cons 'thmname thmname) (cons (cons 'lit-alist lit-alist) (cons (cons 'syntaxp syntaxp) nil))))