Editions of the Verilog or SystemVerilog standards that VL attempts to implement.
Certain parts of VL are configurable and can try follow different versions of the standard. We currently have some support for:
This is an ordinary defenum.
(defun vl-edition-p (x) (declare (xargs :guard t)) (or (eq x ':verilog-2005) (eq x ':system-verilog-2012)))
(defthm type-when-vl-edition-p (implies (vl-edition-p x) (if (symbolp x) (if (not (equal x 't)) (not (equal x 'nil)) 'nil) 'nil)) :rule-classes :compound-recognizer)