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