		Search-engine friendly clone of the ACL2 documentation.

Json-encoders

Jp-sym-main

Encode a simple symbol as a JSON string, including the surrounding quotes.

Signature
(jp-sym-main x &key (ps 'ps)) → ps
Arguments: x — Guard (symbolp x).

We assume that x has a simple enough name to print without any encoding. This is generally true for keyword constants used as tags and in basic enumerations like vl-exprtype-p. We print only the symbol name, in lower-case.

Definitions and Theorems

Function: jp-sym-main-fn

(defun jp-sym-main-fn (x ps)
  (declare (xargs :stobjs (ps)))
  (declare (xargs :guard (symbolp x)))
  (let ((__function__ 'jp-sym-main))
    (declare (ignorable __function__))
    (vl-ps-seq (vl-print "\"")
               (vl-print-str (str::downcase-string (symbol-name x)))
               (vl-print "\""))))