		Search-engine friendly clone of the ACL2 documentation.

Formalized-subset

Declon-obj-formalp

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

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

This complements init-declor-obj-formalp; see the documentation of that function. The declaration must not be a static assertion declaration. We require a single supported initializer declarator. The declaration specifiers must be all type specifiers and storage class specifiers: the former must form a supported sequence, and the latter must be either absent or a single extern. We do not support GCC extensions.

Definitions and Theorems

Function: declon-obj-formalp

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

Theorem: booleanp-of-declon-obj-formalp

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

Theorem: declon-obj-formalp-of-declon-fix-declon

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

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

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