Direction for a port declaration (input, output, or inout).
Each port declaration (see vl-portdecl-p) includes a
direction to indicate that the port is either an input, output, or inout. We
represent these directions with the keyword
This is an ordinary defenum.
(defun vl-direction-p (x) (declare (xargs :guard t)) (or (eq x ':vl-input) (eq x ':vl-output) (eq x ':vl-inout)))
(defthm type-when-vl-direction-p (implies (vl-direction-p x) (if (symbolp x) (if (not (equal x 't)) (not (equal x 'nil)) 'nil) 'nil)) :rule-classes :compound-recognizer)