		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 states that its argument is a character.

Char-downcase 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-downcase

(defun char-downcase (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-downcase-non-standard x))))

Subtopics

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