Vl-expr-p
Recognizer for vl-expr structures.
- Signature
(vl-expr-p x) → *
Definitions and Theorems
Theorem: consp-when-vl-expr-p
(defthm consp-when-vl-expr-p
(implies (vl-expr-p x) (consp x))
:rule-classes :compound-recognizer)
Subtopics
- Vl-expr-lvaluep
- Determine if an expression looks like a good lvalue.
- Welltyped
- Expressions whose sizes and types are sensible.
