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