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