Check if a list of type specifiers has formal dynamic semantics.
(type-spec-list-formalp tyspecs) → yes/no
In the abstract syntax of the formal language definition,
type specifier sequences may occur in
type names,
structure declarations,
parameter declarations,
function declarations,
object declarations,
and function definitions.
For type names, as discussed in type-spec-list-integer-formalp,
there is only support for type specifier sequences
that denote integer types except plain
Function:
(defun type-spec-list-formalp (tyspecs) (declare (xargs :guard (type-spec-listp tyspecs))) (declare (xargs :guard (type-spec-list-unambp tyspecs))) (let ((__function__ 'type-spec-list-formalp)) (declare (ignorable __function__)) (or (type-spec-list-integer-formalp tyspecs) (and (consp tyspecs) (endp (cdr tyspecs)) (type-spec-case (car tyspecs) :struct) (check-strunispec-no-members (type-spec-struct->unwrap (car tyspecs))) t))))
Theorem:
(defthm booleanp-of-type-spec-list-formalp (b* ((yes/no (type-spec-list-formalp tyspecs))) (booleanp yes/no)) :rule-classes :rewrite)
Theorem:
(defthm type-spec-list-formalp-of-type-spec-list-fix-tyspecs (equal (type-spec-list-formalp (type-spec-list-fix tyspecs)) (type-spec-list-formalp tyspecs)))
Theorem:
(defthm type-spec-list-formalp-type-spec-list-equiv-congruence-on-tyspecs (implies (type-spec-list-equiv tyspecs tyspecs-equiv) (equal (type-spec-list-formalp tyspecs) (type-spec-list-formalp tyspecs-equiv))) :rule-classes :congruence)