		Search-engine friendly clone of the ACL2 documentation.

Formalized-subset

Decl-fun-formalp

Check if a declaration has dynamic formal semantics, as a function declaration.

Signature
(decl-fun-formalp decl) → yes/no
Arguments: decl — Guard (declp decl).
Returns: yes/no — Type (booleanp yes/no).

It must not be a static assertion declaration, and there must be no GCC extensions. There may be only type specifiers, for a supported type. There must a single supported initializer declarator.

Definitions and Theorems

Function: decl-fun-formalp

(defun decl-fun-formalp (decl)
 (declare (xargs :guard (declp decl)))
 (declare (xargs :guard (decl-unambp decl)))
 (let ((__function__ 'decl-fun-formalp))
  (declare (ignorable __function__))
  (decl-case
   decl
   :decl (and (not decl.extension)
              (b* (((mv okp tyspecs)
                    (check-decl-spec-list-all-typespec decl.specs)))
                (and okp (type-spec-list-formalp tyspecs)))
              (consp decl.init)
              (endp (cdr decl.init))
              (initdeclor-fun-formalp (car decl.init)))
   :statassert nil)))

Theorem: booleanp-of-decl-fun-formalp

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

Theorem: decl-fun-formalp-of-decl-fix-decl

(defthm decl-fun-formalp-of-decl-fix-decl
  (equal (decl-fun-formalp (decl-fix decl))
         (decl-fun-formalp decl)))

Theorem: decl-fun-formalp-decl-equiv-congruence-on-decl

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