		Search-engine friendly clone of the ACL2 documentation.

@formals

Construct an XDOC tree for a formals directive @(formals ...).

Macro: @formals

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

Function: @formals-fn

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

Theorem: stringp-of-@formals

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