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