		Search-engine friendly clone of the ACL2 documentation.

@gdef

Construct an XDOC tree for a generated definition directive @(gdef ...).

Macro: @gdef

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

Function: @gdef-fn

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

Theorem: stringp-of-@gdef

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