Extract the list of storage class specifiers from a list of declaration specifiers, preserving the order.
(declspec-list-to-stor-spec-list declspecs) → stor-specs
Function:
(defun declspec-list-to-stor-spec-list (declspecs) (declare (xargs :guard (declspec-listp declspecs))) (let ((__function__ 'declspec-list-to-stor-spec-list)) (declare (ignorable __function__)) (b* (((when (endp declspecs)) nil) (declspec (car declspecs))) (if (declspec-case declspec :stocla) (cons (declspec-stocla->unwrap declspec) (declspec-list-to-stor-spec-list (cdr declspecs))) (declspec-list-to-stor-spec-list (cdr declspecs))))))
Theorem:
(defthm stor-spec-listp-of-declspec-list-to-stor-spec-list (b* ((stor-specs (declspec-list-to-stor-spec-list declspecs))) (stor-spec-listp stor-specs)) :rule-classes :rewrite)
Theorem:
(defthm declspec-list-to-stor-spec-list-of-declspec-list-fix-declspecs (equal (declspec-list-to-stor-spec-list (declspec-list-fix declspecs)) (declspec-list-to-stor-spec-list declspecs)))
Theorem:
(defthm declspec-list-to-stor-spec-list-declspec-list-equiv-congruence-on-declspecs (implies (declspec-list-equiv declspecs declspecs-equiv) (equal (declspec-list-to-stor-spec-list declspecs) (declspec-list-to-stor-spec-list declspecs-equiv))) :rule-classes :congruence)