Decompose a structure declaration into an identifier and a type name.
(struct-declon-to-ident+tyname declon) → (mv id tyname)
Function:
(defun struct-declon-to-ident+tyname (declon) (declare (xargs :guard (struct-declonp declon))) (let ((__function__ 'struct-declon-to-ident+tyname)) (declare (ignorable __function__)) (b* (((struct-declon declon) declon)) (tyspec+declor-to-ident+tyname declon.tyspec declon.declor))))
Theorem:
(defthm identp-of-struct-declon-to-ident+tyname.id (b* (((mv acl2::?id ?tyname) (struct-declon-to-ident+tyname declon))) (identp id)) :rule-classes :rewrite)
Theorem:
(defthm tynamep-of-struct-declon-to-ident+tyname.tyname (b* (((mv acl2::?id ?tyname) (struct-declon-to-ident+tyname declon))) (tynamep tyname)) :rule-classes :rewrite)
Theorem:
(defthm struct-declon-to-ident+tyname-of-struct-declon-fix-declon (equal (struct-declon-to-ident+tyname (struct-declon-fix declon)) (struct-declon-to-ident+tyname declon)))
Theorem:
(defthm struct-declon-to-ident+tyname-struct-declon-equiv-congruence-on-declon (implies (struct-declon-equiv declon declon-equiv) (equal (struct-declon-to-ident+tyname declon) (struct-declon-to-ident+tyname declon-equiv))) :rule-classes :congruence)