		Search-engine friendly clone of the ACL2 documentation.

Charset-p

Str-count-leading-charset

String version of count-leading-charset.

Signature
(str-count-leading-charset n x xl set) → n
Arguments: n — Current position in the string.
Guard (natp n).; x — String we're iterating through.
Guard (stringp x).; xl — Precomputed length of x.
Guard (eql xl (length x)).; set — Set of characters we're counting.
Guard (charset-p set).
Returns: n — Type (natp n).

Definitions and Theorems

Function: str-count-leading-charset

(defun str-count-leading-charset (n x xl set)
  (declare (xargs :guard (and (natp n)
                              (stringp x)
                              (charset-p set)
                              (eql xl (length x)))))
  (declare (type (integer 0 *) xl n)
           (type string x))
  (declare (xargs :guard (<= n xl)))
  (let ((acl2::__function__ 'str-count-leading-charset))
    (declare (ignorable acl2::__function__))
    (mbe :logic
         (let ((chars (nthcdr n (coerce x 'list))))
           (count-leading-charset chars set))
         :exec
         (b* (((when (eql n xl)) 0)
              ((the character char1) (char x n))
              ((when (char-in-charset-p char1 set))
               (+ 1
                  (str-count-leading-charset (+ 1 n)
                                             x xl set))))
           0))))

Theorem: natp-of-str-count-leading-charset

(defthm natp-of-str-count-leading-charset
  (b* ((n (str-count-leading-charset n x xl set)))
    (natp n))
  :rule-classes :type-prescription)