Recognizer for vl-paramtype structures.
(vl-paramtype-p x) → *
Function:
(defun vl-paramtype-p (x) (declare (xargs :guard t)) (let ((__function__ 'vl-paramtype-p)) (declare (ignorable __function__)) (and (consp x) (cond ((or (atom x) (eq (car x) :vl-implicitvalueparam)) (and (std::prod-consp (cdr x)) (std::prod-consp (std::prod-cdr (cdr x))) (b* ((range (std::prod-car (cdr x))) (sign (std::prod-car (std::prod-cdr (cdr x)))) (default (std::prod-cdr (std::prod-cdr (cdr x))))) (and (vl-maybe-range-p range) (vl-maybe-exprsign-p sign) (vl-maybe-expr-p default))))) ((eq (car x) :vl-explicitvalueparam) (and (std::prod-consp (cdr x)) (std::prod-consp (std::prod-cdr (cdr x))) (b* ((type (std::prod-car (cdr x))) (default (std::prod-car (std::prod-cdr (cdr x)))) (final-value (std::prod-cdr (std::prod-cdr (cdr x))))) (and (vl-datatype-p type) (vl-maybe-expr-p default) (sv::maybe-4vec-p final-value))))) (t (and (eq (car x) :vl-typeparam) (and) (b* ((default (cdr x))) (vl-maybe-datatype-p default))))))))
Theorem:
(defthm consp-when-vl-paramtype-p (implies (vl-paramtype-p x) (consp x)) :rule-classes :compound-recognizer)