		Search-engine friendly clone of the ACL2 documentation.

Formalized-subset

Declon-fun-formalp

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

Signature
(declon-fun-formalp declon) → yes/no
Arguments: declon — Guard (declonp declon).
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: declon-fun-formalp

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

Theorem: booleanp-of-declon-fun-formalp

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

Theorem: declon-fun-formalp-of-declon-fix-declon

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

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

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