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