		Search-engine friendly clone of the ACL2 documentation.

Formalized-subset

Init-declor-fun-formalp

Check if an initializer declarator has formal dynamic semantics, as part of a function declaration.

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

There must be no initializer, and the declarator must be supported. There must be no assembler name specifier and no attribute specifiers.

Definitions and Theorems

Function: init-declor-fun-formalp

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

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

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

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

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

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

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