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