Check if an initializer with optional designations has formal dynamic semantics.
(desiniter-formalp desiniter) → yes/no
Since compound literals are not supported currently,
the only place where initializers with optional designations occur
is as elements of list initializers
(i.e. the
Function:
(defun desiniter-formalp (desiniter) (declare (xargs :guard (desiniterp desiniter))) (declare (xargs :guard (desiniter-unambp desiniter))) (let ((__function__ 'desiniter-formalp)) (declare (ignorable __function__)) (b* (((desiniter desiniter) desiniter)) (and (endp desiniter.design) (initer-case desiniter.init :single) (expr-pure-formalp (initer-single->expr desiniter.init))))))
Theorem:
(defthm booleanp-of-desiniter-formalp (b* ((yes/no (desiniter-formalp desiniter))) (booleanp yes/no)) :rule-classes :rewrite)
Theorem:
(defthm desiniter-formalp-of-desiniter-fix-desiniter (equal (desiniter-formalp (desiniter-fix desiniter)) (desiniter-formalp desiniter)))
Theorem:
(defthm desiniter-formalp-desiniter-equiv-congruence-on-desiniter (implies (desiniter-equiv desiniter desiniter-equiv) (equal (desiniter-formalp desiniter) (desiniter-formalp desiniter-equiv))) :rule-classes :congruence)