Check if an optional token may start an expression.
(token-expression-start-p token?) → yes/no
Looking at the grammar, an expression always starts with (or is) a cast expression, which is either a unary expression or a cast expression proper. The latter starts with an open parenthesis, but that is already covered by the possible starts of primary expressions.
So we just define this as a synonym of token-unary-expression-start-p, to make it clearer that we are talking about all expressions and not just unary expressions.
Function:
(defun token-expression-start-p (token?) (declare (xargs :guard (token-optionp token?))) (let ((__function__ 'token-expression-start-p)) (declare (ignorable __function__)) (token-unary-expression-start-p token?)))
Theorem:
(defthm booleanp-of-token-expression-start-p (b* ((yes/no (token-expression-start-p token?))) (booleanp yes/no)) :rule-classes :rewrite)
Theorem:
(defthm non-nil-when-token-expression-start-p (implies (token-expression-start-p token?) token?) :rule-classes :compound-recognizer)