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