Function:
(defun vl-echarlist-from-str-nice (x n xl filename line col) (declare (xargs :guard (and (stringp x) (natp n) (stringp filename) (posp line) (natp col) (equal xl (length x))))) (declare (type string x filename) (type integer n xl line col)) (declare (xargs :split-types t :guard (<= n xl))) (let ((__function__ 'vl-echarlist-from-str-nice)) (declare (ignorable __function__)) (mbe :logic (b* (((when (zp (- (nfix xl) (nfix n)))) nil) (char (char-fix (char x n))) (line (pos-fix line)) (col (nfix col)) (echar (make-vl-echar-fast :char char :filename filename :line line :col col))) (cons echar (vl-echarlist-from-str-nice x (+ 1 (nfix n)) xl filename (if (eql char #\Newline) (+ 1 line) line) (if (eql char #\Newline) 0 (+ 1 col))))) :exec (with-local-nrev (vl-echarlist-from-str-aux x n xl filename line col nrev)))))
Theorem:
(defthm vl-echarlist-from-str-aux-correct (implies (and (posp line) (natp col)) (equal (vl-echarlist-from-str-aux x n xl filename line col acc) (append acc (vl-echarlist-from-str-nice x n xl filename line col)))))
Theorem:
(defthm vl-echarlist-from-str-nice-correct (equal (vl-echarlist-from-str-nice x n (len (explode x)) filename line col) (vl-echarlist-from-chars-fn (nthcdr n (explode x)) filename line col)))
Theorem:
(defthm vl-echarlist-from-str-nice-of-str-fix-x (equal (vl-echarlist-from-str-nice (str-fix x) n xl filename line col) (vl-echarlist-from-str-nice x n xl filename line col)))
Theorem:
(defthm vl-echarlist-from-str-nice-streqv-congruence-on-x (implies (streqv x x-equiv) (equal (vl-echarlist-from-str-nice x n xl filename line col) (vl-echarlist-from-str-nice x-equiv n xl filename line col))) :rule-classes :congruence)
Theorem:
(defthm vl-echarlist-from-str-nice-of-nfix-n (equal (vl-echarlist-from-str-nice x (nfix n) xl filename line col) (vl-echarlist-from-str-nice x n xl filename line col)))
Theorem:
(defthm vl-echarlist-from-str-nice-nat-equiv-congruence-on-n (implies (acl2::nat-equiv n n-equiv) (equal (vl-echarlist-from-str-nice x n xl filename line col) (vl-echarlist-from-str-nice x n-equiv xl filename line col))) :rule-classes :congruence)
Theorem:
(defthm vl-echarlist-from-str-nice-of-str-fix-filename (equal (vl-echarlist-from-str-nice x n xl (str-fix filename) line col) (vl-echarlist-from-str-nice x n xl filename line col)))
Theorem:
(defthm vl-echarlist-from-str-nice-streqv-congruence-on-filename (implies (streqv filename filename-equiv) (equal (vl-echarlist-from-str-nice x n xl filename line col) (vl-echarlist-from-str-nice x n xl filename-equiv line col))) :rule-classes :congruence)
Theorem:
(defthm vl-echarlist-from-str-nice-of-pos-fix-line (equal (vl-echarlist-from-str-nice x n xl filename (pos-fix line) col) (vl-echarlist-from-str-nice x n xl filename line col)))
Theorem:
(defthm vl-echarlist-from-str-nice-pos-equiv-congruence-on-line (implies (acl2::pos-equiv line line-equiv) (equal (vl-echarlist-from-str-nice x n xl filename line col) (vl-echarlist-from-str-nice x n xl filename line-equiv col))) :rule-classes :congruence)
Theorem:
(defthm vl-echarlist-from-str-nice-of-nfix-col (equal (vl-echarlist-from-str-nice x n xl filename line (nfix col)) (vl-echarlist-from-str-nice x n xl filename line col)))
Theorem:
(defthm vl-echarlist-from-str-nice-nat-equiv-congruence-on-col (implies (acl2::nat-equiv col col-equiv) (equal (vl-echarlist-from-str-nice x n xl filename line col) (vl-echarlist-from-str-nice x n xl filename line col-equiv))) :rule-classes :congruence)