		Search-engine friendly clone of the ACL2 documentation.

Formalized-subset

Declon-block-formalp

Check if a declaration has formal dynamic semantics, as a block item.

Signature
(declon-block-formalp declon) → yes/no
Arguments: declon — Guard (declonp declon).
Returns: yes/no — Type (booleanp yes/no).

The declaration must not be a static assertion declaration. The GCC extensions must be absent, since they are not covered by our formal semantics. All the declaration specifiers must be type specifiers, because c::exec-block-item does not support storage class specifiers; the type specifier sequence must be a supported one. There must be exactly one supported initializer declarator.

Definitions and Theorems

Function: declon-block-formalp

(defun declon-block-formalp (declon)
 (declare (xargs :guard (declonp declon)))
 (declare (xargs :guard (declon-unambp declon)))
 (let ((__function__ 'declon-block-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-block-formalp (car declon.declors)))
       :statassert nil)))

Theorem: booleanp-of-declon-block-formalp

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

Theorem: declon-block-formalp-of-declon-fix-declon

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

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

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