		Search-engine friendly clone of the ACL2 documentation.

Cases

Downcase-first

Convert the first character of a string to lower case.

Signature
(downcase-first x) → downcased
Returns: downcased — Type (stringp downcased).

(downcase-first x) returns a copy of the string x except that the first character is downcased using downcase-char. If the string is empty, we return it unchanged.

For sometimes-better performance, we avoid consing and simply return x unchanged when its first character is not an upper-case letter.

Definitions and Theorems

Function: downcase-first

(defun
    downcase-first (x)
    (declare (type string x))
    (let ((acl2::__function__ 'downcase-first))
         (declare (ignorable acl2::__function__))
         (mbe :logic (implode (downcase-first-charlist (explode x)))
              :exec (if (eql (length x) 0)
                        x
                        (let ((c (char x 0)))
                             (if (up-alpha-p c)
                                 (cat (downcase-char-str c)
                                      (subseq x 1 nil))
                                 x))))))

Theorem: stringp-of-downcase-first

(defthm stringp-of-downcase-first
        (b* ((downcased (downcase-first x)))
            (stringp downcased))
        :rule-classes :type-prescription)

Theorem: streqv-implies-equal-downcase-first-1

(defthm streqv-implies-equal-downcase-first-1
        (implies (streqv x x-equiv)
                 (equal (downcase-first x)
                        (downcase-first x-equiv)))
        :rule-classes (:congruence))

Theorem: istreqv-implies-istreqv-downcase-first-1

(defthm istreqv-implies-istreqv-downcase-first-1
        (implies (istreqv x x-equiv)
                 (istreqv (downcase-first x)
                          (downcase-first x-equiv)))
        :rule-classes (:congruence))