		Search-engine friendly clone of the ACL2 documentation.

Cases

Upcase-char-str

Convert a character into an upper-case one-element string.

Signature
(upcase-char-str c) → str
Arguments: c — Guard (characterp c).
Returns: str — Type (stringp str).

(upcase-char-str c) is logically equal to:

(implode (list (upcase-char c)))

But we store these strings in a table so that they don't have to be recomputed. This is mainly useful to reduce the creation of temporary strings during upcase-first.

Definitions and Theorems

Function: make-upcase-first-strtbl

(defun make-upcase-first-strtbl (n)
       (declare (xargs :guard (and (natp n) (<= n 255))))
       (cons (cons n
                   (implode (list (upcase-char (code-char n)))))
             (if (zp n)
                 nil
                 (make-upcase-first-strtbl (- n 1)))))

Function: upcase-char-str$inline

(defun
     upcase-char-str$inline (c)
     (declare (xargs :guard (characterp c)))
     (let ((acl2::__function__ 'upcase-char-str))
          (declare (ignorable acl2::__function__))
          (mbe :logic (implode (list (upcase-char c)))
               :exec (aref1 '*upcase-first-strtbl*
                            *upcase-first-strtbl* (char-code c)))))

Theorem: stringp-of-upcase-char-str

(defthm stringp-of-upcase-char-str
        (b* ((str (upcase-char-str$inline c)))
            (stringp str))
        :rule-classes :type-prescription)