Decompose an object declaration into an identifier, a storage class specifier sequence, a type name, and an optional initializer.
(obj-declon-to-ident+scspec+tyname+init declon) → (mv id scspec tyname init)
Function:
(defun obj-declon-to-ident+scspec+tyname+init (declon) (declare (xargs :guard (obj-declonp declon))) (let ((__function__ 'obj-declon-to-ident+scspec+tyname+init)) (declare (ignorable __function__)) (b* (((obj-declon declon) declon) ((mv id tyname) (tyspec+declor-to-ident+tyname declon.tyspec declon.declor))) (mv id declon.scspec tyname declon.init?))))
Theorem:
(defthm identp-of-obj-declon-to-ident+scspec+tyname+init.id (b* (((mv acl2::?id ?scspec ?tyname ?init) (obj-declon-to-ident+scspec+tyname+init declon))) (identp id)) :rule-classes :rewrite)
Theorem:
(defthm scspecseqp-of-obj-declon-to-ident+scspec+tyname+init.scspec (b* (((mv acl2::?id ?scspec ?tyname ?init) (obj-declon-to-ident+scspec+tyname+init declon))) (scspecseqp scspec)) :rule-classes :rewrite)
Theorem:
(defthm tynamep-of-obj-declon-to-ident+scspec+tyname+init.tyname (b* (((mv acl2::?id ?scspec ?tyname ?init) (obj-declon-to-ident+scspec+tyname+init declon))) (tynamep tyname)) :rule-classes :rewrite)
Theorem:
(defthm initer-optionp-of-obj-declon-to-ident+scspec+tyname+init.init (b* (((mv acl2::?id ?scspec ?tyname ?init) (obj-declon-to-ident+scspec+tyname+init declon))) (initer-optionp init)) :rule-classes :rewrite)
Theorem:
(defthm obj-declon-to-ident+scspec+tyname+init-of-obj-declon-fix-declon (equal (obj-declon-to-ident+scspec+tyname+init (obj-declon-fix declon)) (obj-declon-to-ident+scspec+tyname+init declon)))
Theorem:
(defthm obj-declon-to-ident+scspec+tyname+init-obj-declon-equiv-congruence-on-declon (implies (obj-declon-equiv declon declon-equiv) (equal (obj-declon-to-ident+scspec+tyname+init declon) (obj-declon-to-ident+scspec+tyname+init declon-equiv))) :rule-classes :congruence)