Check if a list of storage class specifiers has formal dynamic semantics.
(stor-spec-list-formalp storspecs) → yes/no
We only allow a single
Function:
(defun stor-spec-list-formalp (storspecs) (declare (xargs :guard (stor-spec-listp storspecs))) (let ((__function__ 'stor-spec-list-formalp)) (declare (ignorable __function__)) (b* ((storspecs (stor-spec-list-fix storspecs))) (or (equal storspecs nil) (equal storspecs (list (stor-spec-extern)))))))
Theorem:
(defthm booleanp-of-stor-spec-list-formalp (b* ((yes/no (stor-spec-list-formalp storspecs))) (booleanp yes/no)) :rule-classes :rewrite)
Theorem:
(defthm stor-spec-list-formalp-of-stor-spec-list-fix-storspecs (equal (stor-spec-list-formalp (stor-spec-list-fix storspecs)) (stor-spec-list-formalp storspecs)))
Theorem:
(defthm stor-spec-list-formalp-stor-spec-list-equiv-congruence-on-storspecs (implies (stor-spec-list-equiv storspecs storspecs-equiv) (equal (stor-spec-list-formalp storspecs) (stor-spec-list-formalp storspecs-equiv))) :rule-classes :congruence)