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