(vl-tokstream->pstate &key (tokstream 'tokstream)) → pstate
Function:
(defun vl-tokstream->pstate$inline (tokstream) (declare (xargs :stobjs (tokstream))) (declare (xargs :guard t)) (let ((__function__ 'vl-tokstream->pstate)) (declare (ignorable __function__)) (mbe :logic (vl-parsestate-fix (vl-tokstream->pstate-raw tokstream)) :exec (vl-tokstream->pstate-raw tokstream))))
Theorem:
(defthm vl-parsestate-p-of-vl-tokstream->pstate (b* ((pstate (vl-tokstream->pstate$inline tokstream))) (vl-parsestate-p pstate)) :rule-classes :rewrite)