Check if a type name has formal dynamic semantics.
In the abstract syntax of the formal language definition,
type names are only used in cast expressions,
which are required by c::eval-cast to denote integer types
(except the plain
Function:
(defun tyname-formalp (tyname) (declare (xargs :guard (tynamep tyname))) (declare (xargs :guard (tyname-unambp tyname))) (let ((__function__ 'tyname-formalp)) (declare (ignorable __function__)) (b* (((tyname tyname) tyname) ((mv okp tyspecs) (check-spec/qual-list-all-tyspec tyname.specqual))) (and okp (type-spec-list-integer-formalp tyspecs) (not tyname.decl?)))))
Theorem:
(defthm booleanp-of-tyname-formalp (b* ((yes/no (tyname-formalp tyname))) (booleanp yes/no)) :rule-classes :rewrite)
Theorem:
(defthm tyname-formalp-of-tyname-fix-tyname (equal (tyname-formalp (tyname-fix tyname)) (tyname-formalp tyname)))
Theorem:
(defthm tyname-formalp-tyname-equiv-congruence-on-tyname (implies (tyname-equiv tyname tyname-equiv) (equal (tyname-formalp tyname) (tyname-formalp tyname-equiv))) :rule-classes :congruence)