Extend the parse state to record that there is a new user-defined type.
(vl-parsestate-add-user-defined-type name pstate) → new-pstate
Function:
(defun vl-parsestate-add-user-defined-type (name pstate) (declare (xargs :guard (and (stringp name) (vl-parsestate-p pstate)))) (let ((__function__ 'vl-parsestate-add-user-defined-type)) (declare (ignorable __function__)) (b* (((vl-parsestate pstate) pstate) (new-usertypes (hons-acons name t pstate.usertypes))) (change-vl-parsestate pstate :usertypes new-usertypes))))
Theorem:
(defthm vl-parsestate-p-of-vl-parsestate-add-user-defined-type (b* ((new-pstate (vl-parsestate-add-user-defined-type name pstate))) (vl-parsestate-p new-pstate)) :rule-classes :rewrite)