		Search-engine friendly clone of the ACL2 documentation.

Char-downcase

Turn upper-case characters into lower-case characters

(Char-downcase 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-downcase requires its argument to be a standard character (see standard-char-p).

Char-downcase is a Common Lisp function. See any Common Lisp documentation for more information.

Function: char-downcase

(defun char-downcase (x)
       (declare (xargs :guard (and (characterp x)
                                   (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))
                  ((characterp x) x)
                  (t (code-char 0)))))

Subtopics

Downcase-char: Convert a character to lower-case.