(vl-parse-expression-top &key (tokens 'tokens) (pstate 'pstate) (config 'config)) → (mv erp result tokens pstate)
Function:
(defun vl-parse-expression-top-fn (tokens pstate config) (declare (xargs :guard (and (vl-tokenlist-p tokens) (vl-parsestate-p pstate) (vl-loadconfig-p config)))) (declare (xargs :guard t)) (let ((__function__ 'vl-parse-expression-top)) (declare (ignorable __function__)) (b* (((local-stobjs tokstream) (mv erp result tokens pstate tokstream)) (tokstream (vl-tokstream-update-tokens tokens)) (tokstream (vl-tokstream-update-pstate pstate)) ((mv erp result tokstream) (vl-parse-expression))) (mv erp result (vl-tokstream->tokens) (vl-tokstream->pstate) tokstream))))
Theorem:
(defthm return-type-of-vl-parse-expression-top.result (b* (((mv ?erp ?result ?tokens ?pstate) (vl-parse-expression-top-fn tokens pstate config))) (implies (and (not erp) t) (vl-expr-p result))) :rule-classes :rewrite)
Theorem:
(defthm vl-tokenlist-p-of-vl-parse-expression-top.tokens (b* (((mv ?erp ?result ?tokens ?pstate) (vl-parse-expression-top-fn tokens pstate config))) (vl-tokenlist-p tokens)) :rule-classes :rewrite)
Theorem:
(defthm vl-parsestate-p-of-vl-parse-expression-top.pstate (b* (((mv ?erp ?result ?tokens ?pstate) (vl-parse-expression-top-fn tokens pstate config))) (vl-parsestate-p pstate)) :rule-classes :rewrite)