		Search-engine friendly clone of the ACL2 documentation.

Formalized-subset

Initer-formalp

Check if an initializer has formal dynamic semantics.

Signature
(initer-formalp initer) → yes/no
Arguments: initer — Guard (initerp initer).
Returns: yes/no — Type (booleanp yes/no).

This is based on c::exec-initer. If the initializer is a single expression, the expression must be a supported call or pure expression. If the initializer is a list, each element of the list must be a supported pure expressions.

Definitions and Theorems

Function: initer-formalp

(defun initer-formalp (initer)
  (declare (xargs :guard (initerp initer)))
  (declare (xargs :guard (initer-unambp initer)))
  (let ((__function__ 'initer-formalp))
    (declare (ignorable __function__))
    (initer-case initer
                 :single (or (expr-pure-formalp initer.expr)
                             (expr-call-formalp initer.expr))
                 :list (desiniter-list-formalp initer.elems))))

Theorem: booleanp-of-initer-formalp

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

Theorem: initer-formalp-of-initer-fix-initer

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

Theorem: initer-formalp-initer-equiv-congruence-on-initer

(defthm initer-formalp-initer-equiv-congruence-on-initer
  (implies (initer-equiv initer initer-equiv)
           (equal (initer-formalp initer)
                  (initer-formalp initer-equiv)))
  :rule-classes :congruence)