		Search-engine friendly clone of the ACL2 documentation.

Cases

Upcase-first

Convert the first character of a string to upper case.

Signature
(upcase-first x) → upcased
Returns: upcased — Type (stringp upcased).

(upcase-first x) returns a copy of the string x except that the first character is upcased using upcase-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 a lower-case letter.

Definitions and Theorems

Function: upcase-first

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

Theorem: stringp-of-upcase-first

(defthm stringp-of-upcase-first
        (b* ((upcased (upcase-first x)))
            (stringp upcased))
        :rule-classes :type-prescription)

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

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

Theorem: istreqv-implies-istreqv-upcase-first-1

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