		Search-engine friendly clone of the ACL2 documentation.

Formalized-subset

Init-declor-obj-formalp

Check if an initializer declarator has formal dynamic semantics, as part of an object declaration (not in a block).

Signature
(init-declor-obj-formalp initdeclor) → yes/no
Arguments: initdeclor — Guard (init-declorp initdeclor).
Returns: yes/no — Type (booleanp yes/no).

This complements declor-obj-formalp; see the documentation of that function. The initializer is optional, but if present it must be supported. There must be no assembler name specifier and no attribute specifiers.

Definitions and Theorems

Function: init-declor-obj-formalp

(defun init-declor-obj-formalp (initdeclor)
  (declare (xargs :guard (init-declorp initdeclor)))
  (declare (xargs :guard (init-declor-unambp initdeclor)))
  (let ((__function__ 'init-declor-obj-formalp))
    (declare (ignorable __function__))
    (b* (((init-declor initdeclor) initdeclor))
      (and (declor-obj-formalp initdeclor.declor)
           (not initdeclor.asm?)
           (endp initdeclor.attribs)
           (or (not initdeclor.initer?)
               (initer-formalp initdeclor.initer?))))))

Theorem: booleanp-of-init-declor-obj-formalp

(defthm booleanp-of-init-declor-obj-formalp
  (b* ((yes/no (init-declor-obj-formalp initdeclor)))
    (booleanp yes/no))
  :rule-classes :rewrite)

Theorem: init-declor-obj-formalp-of-init-declor-fix-initdeclor

(defthm init-declor-obj-formalp-of-init-declor-fix-initdeclor
  (equal (init-declor-obj-formalp (init-declor-fix initdeclor))
         (init-declor-obj-formalp initdeclor)))

Theorem: init-declor-obj-formalp-init-declor-equiv-congruence-on-initdeclor

(defthm
 init-declor-obj-formalp-init-declor-equiv-congruence-on-initdeclor
 (implies (init-declor-equiv initdeclor initdeclor-equiv)
          (equal (init-declor-obj-formalp initdeclor)
                 (init-declor-obj-formalp initdeclor-equiv)))
 :rule-classes :congruence)