		Search-engine friendly clone of the ACL2 documentation.

Formalized-subset

Initdeclor-obj-formalp

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

Signature
(initdeclor-obj-formalp initdeclor) → yes/no
Arguments: initdeclor — Guard (initdeclorp 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: initdeclor-obj-formalp

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

Theorem: booleanp-of-initdeclor-obj-formalp

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

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

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

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

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