		Search-engine friendly clone of the ACL2 documentation.

@[]

Construct an XDOC tree for a long KaTeK directive @([...]).

Macro: @[]

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

Function: @[]-fn

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

Theorem: stringp-of-@[]

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