		Search-engine friendly clone of the ACL2 documentation.

Formalized-subset

Declon-struct-formalp

Check if a declaration has formal dynamic semantics, as a declaration for a structure type.

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

This must not be a static assertion declaration. It must consists of a single type specifier without declarators. The type specifier must be for a structure type, and have a supported structure or union specifier. There must be no GCC extensions.

Definitions and Theorems

Function: declon-struct-formalp

(defun declon-struct-formalp (declon)
 (declare (xargs :guard (declonp declon)))
 (declare (xargs :guard (declon-unambp declon)))
 (let ((__function__ 'declon-struct-formalp))
  (declare (ignorable __function__))
  (declon-case
   declon
   :declon
   (and (not declon.extension)
        (consp declon.specs)
        (endp (cdr declon.specs))
        (decl-spec-case (car declon.specs)
                        :typespec)
        (b* ((tyspec (decl-spec-typespec->spec (car declon.specs))))
          (and (type-spec-case tyspec :struct)
               (b* ((struni-spec (type-spec-struct->spec tyspec)))
                 (and (struni-spec-formalp struni-spec)
                      (endp declon.declors))))))
   :statassert nil)))

Theorem: booleanp-of-declon-struct-formalp

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

Theorem: declon-struct-formalp-of-declon-fix-declon

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

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

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