		Search-engine friendly clone of the ACL2 documentation.

Grammar-printer-implementation

Pretty-print-char-val

Pretty-print a character value notation.

Signature
(pretty-print-char-val charval) → string
Arguments: charval — Guard (char-val-p charval).
Returns: string — Type (common-lisp::stringp string).

Definitions and Theorems

Function: pretty-print-char-val

(defun pretty-print-char-val (charval)
 (declare (xargs :guard (char-val-p charval)))
 (let ((__function__ 'pretty-print-char-val))
   (declare (ignorable __function__))
   (char-val-case
        charval
        :insensitive
        (str::cat (if (char-val-insensitive->iprefix charval)
                      "%i"
                    "")
                  "\"" (char-val-insensitive->get charval)
                  "\"")
        :sensitive (str::cat "%s\"" (char-val-sensitive->get charval)
                             "\""))))

Theorem: stringp-of-pretty-print-char-val

(defthm stringp-of-pretty-print-char-val
  (b* ((string (pretty-print-char-val charval)))
    (common-lisp::stringp string))
  :rule-classes :rewrite)