Check if an optional token may start an abstract declarator.
(token-abstract-declarator-start-p token?) → yes/no
An abstract declarator may start with a pointer, which always starts with a star. An abstract declarator may also start with a direct abstract declarator.
Function:
(defun token-abstract-declarator-start-p (token?) (declare (xargs :guard (token-optionp token?))) (let ((__function__ 'token-abstract-declarator-start-p)) (declare (ignorable __function__)) (or (token-punctuatorp token? "*") (token-direct-abstract-declarator-start-p token?))))
Theorem:
(defthm booleanp-of-token-abstract-declarator-start-p (b* ((yes/no (token-abstract-declarator-start-p token?))) (booleanp yes/no)) :rule-classes :rewrite)
Theorem:
(defthm non-nil-when-token-abstract-declarator-start-p (implies (token-abstract-declarator-start-p token?) token?) :rule-classes :compound-recognizer)