		Search-engine friendly clone of the ACL2 documentation.

Formalized-subset

Desiniter-formalp

Check if an initializer with optional designations has formal dynamic semantics.

Signature
(desiniter-formalp desiniter) → yes/no
Arguments: desiniter — Guard (desiniterp desiniter).
Returns: yes/no — Type (booleanp 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 :list case of initer). The supported initializers are the ones in c::exec-initer, which only supports list initializers that consist of supported pure expressions. So each element of the list must have no designations and be a single supported pure expression.

Definitions and Theorems

Function: desiniter-formalp

(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.designors)
      (initer-case desiniter.initer :single)
      (expr-pure-formalp (initer-single->expr desiniter.initer))))))

Theorem: booleanp-of-desiniter-formalp

(defthm booleanp-of-desiniter-formalp
  (b* ((yes/no (desiniter-formalp desiniter)))
    (booleanp yes/no))
  :rule-classes :rewrite)

Theorem: desiniter-formalp-of-desiniter-fix-desiniter

(defthm desiniter-formalp-of-desiniter-fix-desiniter
  (equal (desiniter-formalp (desiniter-fix desiniter))
         (desiniter-formalp desiniter)))

Theorem: desiniter-formalp-desiniter-equiv-congruence-on-desiniter

(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)