Unread a specified number of tokens.
(unread-tokens n parstate) → new-parstate
This repeatedly calls unread-token
to unread zero or more tokens.
The number of tokens is specified by
Function:
(defun unread-tokens (n parstate) (declare (xargs :stobjs (parstate))) (declare (xargs :guard (and (natp n) (parstatep parstate)))) (let ((__function__ 'unread-tokens)) (declare (ignorable __function__)) (b* (((when (zp n)) (parstate-fix parstate)) (parstate (unread-token parstate))) (unread-tokens (1- n) parstate))))
Theorem:
(defthm parstatep-of-unread-tokens (implies (parstatep parstate) (b* ((new-parstate (unread-tokens n parstate))) (parstatep new-parstate))) :rule-classes :rewrite)
Theorem:
(defthm parsize-of-unread-tokens (b* ((?new-parstate (unread-tokens n parstate))) (equal (parsize new-parstate) (+ (parsize parstate) (nfix n)))))