|
|
|---|
|
|
|
|---|
Construct an XDOC tree for a call directive @(call ...).
Macro:
(defmacro @call (&rest trees) (list '@call-fn (cons 'list trees)))
Function:
(defun @call-fn (trees) (declare (xargs :guard (tree-listp trees))) (make-tree-dir/&& :@call trees))
Theorem:
(defthm stringp-of-@call (equal (treep (@call-fn trees)) (tree-listp trees)))