(vl-plaintokentype-p x) → *
We usually don't need to execute this, but it's used in, e.g., the definition of vl-plaintoken-p, so we probably want it to be fast if we're ever actually running vl-tokenlist-p.
Function:
(defun vl-plaintokentype-p (x) (declare (xargs :guard t)) (let ((__function__ 'vl-plaintokentype-p)) (declare (ignorable __function__)) (consp (hons-get x *vl-plaintoken-fal*))))
Theorem:
(defthm symbolp-when-vl-plaintokentype-p (implies (vl-plaintokentype-p x) (and (symbolp x) (not (equal x t)) (not (equal x nil)))) :rule-classes :compound-recognizer)