Check if all the declaration specifiers in a list are type specifiers.
(check-declspec-list-all-tyspec declspecs) → (mv yes/no tyspecs)
If the check succeeds, also return the list of type specifiers, in the same order.
Function:
(defun check-declspec-list-all-tyspec (declspecs) (declare (xargs :guard (declspec-listp declspecs))) (let ((__function__ 'check-declspec-list-all-tyspec)) (declare (ignorable __function__)) (b* (((when (endp declspecs)) (mv t nil)) (declspec (car declspecs)) ((unless (declspec-case declspec :tyspec)) (mv nil nil)) ((mv yes/no tyspecs) (check-declspec-list-all-tyspec (cdr declspecs)))) (if yes/no (mv t (cons (declspec-tyspec->unwrap declspec) tyspecs)) (mv nil nil)))))
Theorem:
(defthm booleanp-of-check-declspec-list-all-tyspec.yes/no (b* (((mv ?yes/no ?tyspecs) (check-declspec-list-all-tyspec declspecs))) (booleanp yes/no)) :rule-classes :rewrite)
Theorem:
(defthm type-spec-listp-of-check-declspec-list-all-tyspec.tyspecs (b* (((mv ?yes/no ?tyspecs) (check-declspec-list-all-tyspec declspecs))) (type-spec-listp tyspecs)) :rule-classes :rewrite)
Theorem:
(defthm check-declspec-list-all-tyspec-of-declspec-list-fix-declspecs (equal (check-declspec-list-all-tyspec (declspec-list-fix declspecs)) (check-declspec-list-all-tyspec declspecs)))
Theorem:
(defthm check-declspec-list-all-tyspec-declspec-list-equiv-congruence-on-declspecs (implies (declspec-list-equiv declspecs declspecs-equiv) (equal (check-declspec-list-all-tyspec declspecs) (check-declspec-list-all-tyspec declspecs-equiv))) :rule-classes :congruence)