		Search-engine friendly clone of the ACL2 documentation.

Char-upcase

Turn lower-case characters into upper-case characters

(Char-upcase x) is equal to #\A when x is #\a, #\B when x is #\b, ..., and #\Z when x is #\z, and is x for any other character.

The guard for char-upcase states that its argument is a character.

Char-upcase is a Common Lisp function. See any Common Lisp documentation for more information. Note that the value returned may depend on the host Lisp; see soundness, specifically Example 1 in the Section, “Examples of divergence among Lisp implementations”.

Function: char-upcase

(defun char-upcase (x)
  (declare (xargs :guard (characterp x)))
  (cond ((standard-char-p x)
         (let ((pair (assoc x
                            '((#\a . #\A)
                              (#\b . #\B)
                              (#\c . #\C)
                              (#\d . #\D)
                              (#\e . #\E)
                              (#\f . #\F)
                              (#\g . #\G)
                              (#\h . #\H)
                              (#\i . #\I)
                              (#\j . #\J)
                              (#\k . #\K)
                              (#\l . #\L)
                              (#\m . #\M)
                              (#\n . #\N)
                              (#\o . #\O)
                              (#\p . #\P)
                              (#\q . #\Q)
                              (#\r . #\R)
                              (#\s . #\S)
                              (#\t . #\T)
                              (#\u . #\U)
                              (#\v . #\V)
                              (#\w . #\W)
                              (#\x . #\X)
                              (#\y . #\Y)
                              (#\z . #\Z)))))
           (cond (pair (cdr pair)) (t x))))
        (t (char-upcase-non-standard x))))

Subtopics

Upcase-char: Convert a character to upper-case.