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