Function:
(defun scan-for-non-whitespace (idx x) (declare (xargs :guard (and (natp idx) (stringp x)))) (declare (xargs :guard (<= idx (length x)))) (let ((__function__ 'scan-for-non-whitespace)) (declare (ignorable __function__)) (b* (((when (mbe :logic (zp (- (length x) (nfix idx))) :exec (eql idx (length x)))) (mbe :logic (length x) :exec idx)) ((when (not (vl-whitespace-p (char x idx)))) (lnfix idx))) (scan-for-non-whitespace (1+ (lnfix idx)) x))))
Theorem:
(defthm natp-of-scan-for-non-whitespace (b* ((result-idx (scan-for-non-whitespace idx x))) (natp result-idx)) :rule-classes :type-prescription)
Theorem:
(defthm scan-for-non-whitespace-upper-bound (b* ((?result-idx (scan-for-non-whitespace idx x))) (<= result-idx (length x))) :rule-classes :linear)
Theorem:
(defthm scan-for-non-whitespace-finds-non-whitespace (b* ((?result-idx (scan-for-non-whitespace idx x))) (implies (not (equal result-idx (length x))) (not (vl-whitespace-p (char x result-idx))))))
Theorem:
(defthm scan-for-non-whitespace-bound-when-non-whitespace-exists (b* ((?result-idx (scan-for-non-whitespace idx x))) (implies (and (< (nfix nw-idx) (length x)) (not (vl-whitespace-p (char x nw-idx))) (<= (nfix idx) (nfix nw-idx))) (<= result-idx (nfix nw-idx)))))