Check if an initializer declarator has formal dynamic semantics, as part of an object declaration (not in a block).
(initdeclor-obj-formalp initdeclor) → yes/no
This complements declor-obj-formalp; see the documentation of that function. The initializer is optional, but if present it must be supported.
Function:
(defun initdeclor-obj-formalp (initdeclor) (declare (xargs :guard (initdeclorp initdeclor))) (declare (xargs :guard (initdeclor-unambp initdeclor))) (let ((__function__ 'initdeclor-obj-formalp)) (declare (ignorable __function__)) (b* (((initdeclor initdeclor) initdeclor)) (and (declor-obj-formalp initdeclor.declor) (or (not initdeclor.init?) (initer-formalp initdeclor.init?))))))
Theorem:
(defthm booleanp-of-initdeclor-obj-formalp (b* ((yes/no (initdeclor-obj-formalp initdeclor))) (booleanp yes/no)) :rule-classes :rewrite)
Theorem:
(defthm initdeclor-obj-formalp-of-initdeclor-fix-initdeclor (equal (initdeclor-obj-formalp (initdeclor-fix initdeclor)) (initdeclor-obj-formalp initdeclor)))
Theorem:
(defthm initdeclor-obj-formalp-initdeclor-equiv-congruence-on-initdeclor (implies (initdeclor-equiv initdeclor initdeclor-equiv) (equal (initdeclor-obj-formalp initdeclor) (initdeclor-obj-formalp initdeclor-equiv))) :rule-classes :congruence)