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