Variant of quotation introducing templates for data structures
ACL2 supports the backquote (
Together with the use of comma (
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.