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.
Function: kwote
(defun kwote (x)
(declare (xargs :guard t))
(mbe :logic (list 'quote x)
:exec (cond ((eq x nil) *nil*)
((eq x t) *t*)
((eql x 0) *0*)
((eql x 1) *1*)
((eql x -1) *-1*)
(t (list 'quote x)))))
