		Search-engine friendly clone of the ACL2 documentation.

Reader

Backquote

Variant of quotation introducing templates for data structures

ACL2 supports the backquote (`) construct of Common Lisp. See any Common Lisp documentation for details, for example, its discussion in the Common Lisp HyperSpec. Here we give only a brief introduction.

Together with the use of comma (,) and comma-atsign (,@), backquote provides a variant of quote that supports an escape mechanism, as illustrated by the following examples.

ACL2 !>`(a b c)
(A B C)
ACL2 !>(let ((x '(a b c))) `(1 ,(cdr x) 2))
(1 (B C) 2)
ACL2 !>(let ((x '(a b c))) `(1 ,@(cdr x) 2))
(1 B C 2)
ACL2 !>

The first example above illustrates that backquote is much like quote. The second example shows how a comma escapes from the quotation, inserting the value of the object that follows the comma. The third example is similar to the second, except that it uses comma followed by an atsign, which splices in the value (which must satisfy true-listp) rather than inserting it.