		Search-engine friendly clone of the ACL2 documentation.

Down-alpha-p

Determine if a character is a lower-case letter (a-z).

Signature
(down-alpha-p x) → bool

ACL2 has a built-in alternative to this function, common-lisp::lower-case-p, but it is irritating to use because it has standard-char-p guards. In contrast, down-alpha-p works on arbitrary characters.

Definitions and Theorems

Function: down-alpha-p$inline

(defun down-alpha-p$inline (x)
       (declare (type character x))
       (let ((acl2::__function__ 'down-alpha-p))
            (declare (ignorable acl2::__function__))
            (b* (((the (unsigned-byte 8) code)
                  (char-code x)))
                (and (<= (little-a) code)
                     (<= code (little-z))))))

Theorem: chareqv-implies-equal-down-alpha-p-1

(defthm chareqv-implies-equal-down-alpha-p-1
        (implies (chareqv x x-equiv)
                 (equal (down-alpha-p x)
                        (down-alpha-p x-equiv)))
        :rule-classes (:congruence))

Theorem: lower-case-p-is-down-alpha-p

(defthm lower-case-p-is-down-alpha-p
        (equal (common-lisp::lower-case-p x)
               (down-alpha-p (double-rewrite x))))

Theorem: down-alpha-p-when-up-alpha-p

(defthm down-alpha-p-when-up-alpha-p
        (implies (up-alpha-p x)
                 (not (down-alpha-p x))))