		Search-engine friendly clone of the ACL2 documentation.

@srclink

Construct an XDOC tree for a source link directive @(srclink ...).

Macro: @srclink

(defmacro @srclink (&rest trees)
  (list '@srclink-fn (cons 'list trees)))

Function: @srclink-fn

(defun @srclink-fn (trees)
  (declare (xargs :guard (tree-listp trees)))
  (make-tree-dir/&& :@srclink trees))

Theorem: stringp-of-@srclink

(defthm stringp-of-@srclink
  (equal (treep (@srclink-fn trees))
         (tree-listp trees)))