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