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