Check whether some name is the name of a previously-defined, user-defined type.
(vl-parsestate-is-user-defined-type-p name pstate) → user-defined-type-p
Function:
(defun vl-parsestate-is-user-defined-type-p (name pstate) (declare (xargs :guard (and (stringp name) (vl-parsestate-p pstate)))) (let ((__function__ 'vl-parsestate-is-user-defined-type-p)) (declare (ignorable __function__)) (b* (((vl-parsestate pstate) pstate)) (consp (hons-get name pstate.usertypes)))))
Theorem:
(defthm booleanp-of-vl-parsestate-is-user-defined-type-p (b* ((user-defined-type-p (vl-parsestate-is-user-defined-type-p name pstate))) (booleanp user-defined-type-p)) :rule-classes :type-prescription)