Check whether the current token is one of some particular types.
(vl-lookahead-is-some-token? types tokens) → bool
Function:
(defun vl-lookahead-is-some-token?$inline (types tokens) (declare (xargs :guard (and (true-listp types) (vl-tokenlist-p tokens)))) (let ((__function__ 'vl-lookahead-is-some-token?)) (declare (ignorable __function__)) (and (consp tokens) (member-eq (vl-token->type (car tokens)) types) t)))
Theorem:
(defthm vl-lookahead-is-some-token?-when-atom-of-tokens (implies (atom tokens) (equal (vl-lookahead-is-some-token? type tokens) nil)))
Theorem:
(defthm vl-lookahead-is-some-token?-when-atom-of-types (implies (atom types) (equal (vl-lookahead-is-some-token? types tokens) nil)))