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