Find the properties (vl-coredatatype-info structure) for a coretype by its token name (for parsing).
(vl-coretypekwd->info x) → info
Function:
(defun vl-coretypekwd->info (x) (declare (xargs :guard (keywordp x))) (declare (xargs :guard (member-eq x *vl-core-data-type-keywords*))) (let ((__function__ 'vl-coretypekwd->info)) (declare (ignorable __function__)) (vl-coredatatype-infolist-find-kwd x *vl-core-data-type-table*)))
Theorem:
(defthm vl-coredatatype-info-p-of-vl-coretypekwd->info (implies (and (keywordp x) ((lambda (acl2::x acl2::l) (return-last 'acl2::mbe1-raw (acl2::member-eq-exec acl2::x acl2::l) (return-last 'progn (acl2::member-eq-exec$guard-check acl2::x acl2::l) (member-equal acl2::x acl2::l)))) x '(:vl-kwd-string :vl-kwd-event :vl-kwd-chandle :vl-kwd-shortreal :vl-kwd-real :vl-kwd-realtime :vl-kwd-byte :vl-kwd-shortint :vl-kwd-int :vl-kwd-longint :vl-kwd-integer :vl-kwd-time :vl-kwd-bit :vl-kwd-logic :vl-kwd-reg))) (b* ((info (vl-coretypekwd->info x))) (vl-coredatatype-info-p info))) :rule-classes :rewrite)