(to-parstate$-chars-read n parstate) → chars
Function:
(defun to-parstate$-chars-read (n parstate) (declare (xargs :stobjs (parstate))) (declare (xargs :guard (natp n))) (let ((__function__ 'to-parstate$-chars-read)) (declare (ignorable __function__)) (b* (((when (zp n)) nil) (i (1- n)) ((unless (< i (parstate->chars-length parstate))) (raise "Internal error: chars-read index ~x0 out of bound ~x1." i (parstate->chars-length parstate)))) (cons (parstate->char i parstate) (to-parstate$-chars-read (1- n) parstate)))))
Theorem:
(defthm char+position-listp-of-to-parstate$-chars-read (b* ((chars (to-parstate$-chars-read n parstate))) (char+position-listp chars)) :rule-classes :rewrite)