Like nthcdr into a character list, but simultaneously computes the new line and column numbers.
(lc-nthcdr n x line col) → (mv new-chars new-line new-col)
Function:
(defun lc-nthcdr (n x line col) (declare (xargs :guard (and (natp n) (character-listp x) (natp line) (natp col)))) (declare (type (integer 0 *) n line col)) (let ((__function__ 'lc-nthcdr)) (declare (ignorable __function__)) (mbe :logic (mv (nthcdr n x) (line-after-nthcdr n x line) (col-after-nthcdr n x col)) :exec (b* (((when (or (zp n) (atom x))) (mv x line col)) ((the character char1) (car x)) ((the (integer 0 *) n) (- (lnfix n) 1))) (if (eql char1 #\Newline) (lc-nthcdr n (cdr x) (+ 1 line) 0) (lc-nthcdr n (cdr x) line (+ 1 col)))))))