Map a list of storage class specifiers to a storage class specifier sequence in the language definition.
(ldm-stoclaspec-list stoclaspecs) → (mv erp scspecseq)
The list must be empty,
or a singleton with the
Function:
(defun ldm-stoclaspec-list (stoclaspecs) (declare (xargs :guard (stoclaspec-listp stoclaspecs))) (let ((__function__ 'ldm-stoclaspec-list)) (declare (ignorable __function__)) (b* (((reterr) (c::scspecseq-none)) (stoclaspecs (stoclaspec-list-fix stoclaspecs))) (cond ((equal stoclaspecs nil) (retok (c::scspecseq-none))) ((equal stoclaspecs (list (stoclaspec-extern))) (retok (c::scspecseq-extern))) (t (reterr (msg "Unsupported storage class specifier sequence ~x0." stoclaspecs)))))))
Theorem:
(defthm scspecseqp-of-ldm-stoclaspec-list.scspecseq (b* (((mv acl2::?erp ?scspecseq) (ldm-stoclaspec-list stoclaspecs))) (c::scspecseqp scspecseq)) :rule-classes :rewrite)
Theorem:
(defthm ldm-stoclaspec-list-of-stoclaspec-list-fix-stoclaspecs (equal (ldm-stoclaspec-list (stoclaspec-list-fix stoclaspecs)) (ldm-stoclaspec-list stoclaspecs)))
Theorem:
(defthm ldm-stoclaspec-list-stoclaspec-list-equiv-congruence-on-stoclaspecs (implies (stoclaspec-list-equiv stoclaspecs stoclaspecs-equiv) (equal (ldm-stoclaspec-list stoclaspecs) (ldm-stoclaspec-list stoclaspecs-equiv))) :rule-classes :congruence)