Check whether an expression has any attributes.
The parser uses this to ensure that we don't encounter any nested attributes.
Theorem:
(defthm booleanp-of-vl-expr-has-any-atts-p (b* ((bool (vl-expr-has-any-atts-p x))) (booleanp bool)) :rule-classes :type-prescription)
Theorem:
(defthm booleanp-of-vl-expr-has-any-atts-p (b* ((bool (vl-expr-has-any-atts-p x))) (booleanp bool)) :rule-classes :type-prescription)
Theorem:
(defthm booleanp-of-vl-exprlist-has-any-atts-p (b* ((bool (vl-exprlist-has-any-atts-p x))) (booleanp bool)) :rule-classes :type-prescription)