Just used for sanity checking.
(vl-lexstate->plainalist x) → al
Function:
(defun vl-lexstate->plainalist (x) (declare (xargs :guard (vl-lexstate-p x))) (let ((__function__ 'vl-lexstate->plainalist)) (declare (ignorable __function__)) (b* (((vl-lexstate x) x)) (append-without-guard x.bangops x.poundops x.remops x.andops x.starops x.plusops x.dashops x.dotops x.divops x.colonops x.lessops x.gtops x.eqops x.xorops x.barops x.dollarops))))
Theorem:
(defthm vl-plaintoken-alistp-of-vl-lexstate->plainalist (implies (and (force (vl-lexstate-p x))) (b* ((al (vl-lexstate->plainalist x))) (vl-plaintoken-alistp al))) :rule-classes :rewrite)