(update-parstate->token i token+span parstate) → parstate
Function:
(defun update-parstate->token (i token+span parstate) (declare (xargs :stobjs (parstate))) (declare (xargs :guard (and (natp i) (token+span-p token+span)))) (declare (xargs :guard (< i (parstate->tokens-length parstate)))) (let ((__function__ 'update-parstate->token)) (declare (ignorable __function__)) (b* ((parstate (parstate-fix parstate))) (mbe :logic (if (< (nfix i) (parstate->tokens-length parstate)) (raw-update-parstate->token (nfix i) (token+span-fix token+span) parstate) parstate) :exec (raw-update-parstate->token i token+span parstate)))))
Theorem:
(defthm parstatep-of-update-parstate->token (b* ((parstate (update-parstate->token i token+span parstate))) (parstatep parstate)) :rule-classes :rewrite)