		Search-engine friendly clone of the ACL2 documentation.

@{}

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