Check if an initializer declarator has formal dynamic semantics, as part of a function declaration.
(initdeclor-fun-formalp initdeclor) → yes/no
There must be no initializer, and the declarator must be supported.
Function:
(defun initdeclor-fun-formalp (initdeclor) (declare (xargs :guard (initdeclorp initdeclor))) (declare (xargs :guard (initdeclor-unambp initdeclor))) (let ((__function__ 'initdeclor-fun-formalp)) (declare (ignorable __function__)) (b* (((initdeclor initdeclor) initdeclor)) (and (declor-fun-formalp initdeclor.declor) (not initdeclor.asm?) (not initdeclor.init?)))))
Theorem:
(defthm booleanp-of-initdeclor-fun-formalp (b* ((yes/no (initdeclor-fun-formalp initdeclor))) (booleanp yes/no)) :rule-classes :rewrite)
Theorem:
(defthm initdeclor-fun-formalp-of-initdeclor-fix-initdeclor (equal (initdeclor-fun-formalp (initdeclor-fix initdeclor)) (initdeclor-fun-formalp initdeclor)))
Theorem:
(defthm initdeclor-fun-formalp-initdeclor-equiv-congruence-on-initdeclor (implies (initdeclor-equiv initdeclor initdeclor-equiv) (equal (initdeclor-fun-formalp initdeclor) (initdeclor-fun-formalp initdeclor-equiv))) :rule-classes :congruence)