		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))