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