		Search-engine friendly clone of the ACL2 documentation.

@measure

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

Macro: @measure

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

Function: @measure-fn

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

Theorem: stringp-of-@measure

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