The various kinds of basic, atomic, built-in SystemVerilog types.
This is an ordinary defenum.
Function:
(defun vl-basictypekind-p (x) (declare (xargs :guard t)) (or (eq x ':vl-byte) (eq x ':vl-shortint) (eq x ':vl-int) (eq x ':vl-longint) (eq x ':vl-integer) (eq x ':vl-time) (eq x ':vl-bit) (eq x ':vl-logic) (eq x ':vl-reg) (eq x ':vl-shortreal) (eq x ':vl-real) (eq x ':vl-realtime) (eq x ':vl-signed) (eq x ':vl-unsigned) (eq x ':vl-string) (eq x ':vl-const)))
Theorem: type-when-vl-basictypekind-p
(defthm type-when-vl-basictypekind-p (implies (vl-basictypekind-p x) (if (symbolp x) (if (not (equal x 't)) (not (equal x 'nil)) 'nil) 'nil)) :rule-classes :compound-recognizer)