KWOTE

quote an arbitrary object 
Major Section:  ACL2-BUILT-INS

For any object x, (kwote x) returns the two-element list whose elements are the symbol quote and the given x, respectively. The guard of (kwote x) is t.

To see the ACL2 definition of this function, see pf.