		Search-engine friendly clone of the ACL2 documentation.

@$$

Construct an XDOC tree for a short 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)))