Fixnum optimized version of str-count-leading-charset.
(str-count-leading-charset-fast n x xl set) → n
Function:
(defun str-count-leading-charset-fast (n x xl set) (declare (xargs :guard (and (natp n) (stringp x) (charset-p set) (eql xl (length x))))) (declare (type (unsigned-byte 60) n xl) (type string x)) (declare (xargs :guard (<= n xl))) (let ((acl2::__function__ 'str-count-leading-charset-fast)) (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)) ((the (unsigned-byte 60) n) (+ 1 n)) ((when (char-in-charset-p char1 set)) (the (integer 0 *) (+ 1 (str-count-leading-charset-fast n x xl set))))) 0))))
Theorem:
(defthm natp-of-str-count-leading-charset-fast (b* ((n (str-count-leading-charset-fast n x xl set))) (natp n)) :rule-classes :type-prescription)