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