|
|
|---|
|
|
|
|---|
Construct an XDOC tree for a definition directive @(def ...).
Macro:
(defmacro @def (&rest trees) (list '@def-fn (cons 'list trees)))
Function:
(defun @def-fn (trees) (declare (xargs :guard (tree-listp trees))) (make-tree-dir/&& :@def trees))
Theorem:
(defthm stringp-of-@def (equal (treep (@def-fn trees)) (tree-listp trees)))