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
In our argresolve transformation, directions are also assigned to all arguments of gate instances and most arguments of module instances. See our vl-plainarg-p structures for more information.
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)