		Search-engine friendly clone of the ACL2 documentation.

Upcase-string

Upcase-string-aux

Signature
(upcase-string-aux x n xl acc) → *
Arguments: x — Guard (stringp x).; n — Guard (natp n).; xl — Guard (eql xl (length x)).

Definitions and Theorems

Function: upcase-string-aux

(defun upcase-string-aux (x n xl acc)
  (declare (type string x)
           (type (integer 0 *) n)
           (type (integer 0 *) xl))
  (declare (xargs :guard (and (stringp x)
                              (natp n)
                              (eql xl (length x)))))
  (declare (xargs :split-types t :guard (<= n xl)))
  (let ((acl2::__function__ 'upcase-string-aux))
    (declare (ignorable acl2::__function__))
    (mbe :logic
         (revappend (upcase-charlist (nthcdr n (explode x)))
                    acc)
         :exec
         (b* (((when (eql n xl)) acc)
              (char (char x n))
              (upchar (upcase-char char))
              ((the unsigned-byte n) (+ 1 n)))
           (upcase-string-aux x n xl (cons upchar acc))))))