		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.