Major Section: ACL2-BUILT-INS
The form (quote x) evaluates to x. See any Common Lisp documentation.
(quote x)
x
