		Search-engine friendly clone of the ACL2 documentation.

Defmacroq

Define a macro that quotes arguments not wrapped in :eval

Defmacroq has the same general form as defmacro (see defmacro), that is:

(defmacro name macro-args doc-string dcl ... dcl body)

However, for any subsequent call of name, and for each variable var introduced by macro-args that is bound to a corresponding value val from the call, var is instead bound to (quote val) with one exception: if val is of the form (:eval x), then var is bound to the expression x. The following example shows how this works.

ACL2 !>(defmacroq mac2 (x y)
         `(list ,x ,y))

Summary
Form:  ( DEFMACRO MAC2 ...)
Rules: NIL
Time:  0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
 MAC2
ACL2 !>:trans1 (mac2 (a b) (:eval (append '(c d) '(e f))))
 (LIST '(A B) (APPEND '(C D) '(E F)))
ACL2 !>(mac2 (a b) (:eval (append '(c d) '(e f))))
((A B) (C D E F))
ACL2 !>

Thus, if we ignore the role of :eval, the macro definition above is equivalent to the following.

(defmacro mac2 (x y)
  `(list ',x ',y))