		Search-engine friendly clone of the ACL2 documentation.

Formalized-subset

Structdecl-formalp

Check if a structure declaration has formal dynamic semantics.

Signature
(structdecl-formalp structdecl) → yes/no
Arguments: structdecl — Guard (structdeclp structdecl).
Returns: yes/no — Type (booleanp yes/no).

This must be a declaration for a member, not a static assertion. There must be no GCC extension. There must be only type specifiers, not type qualifiers, and they must form a supported type. There must be a single supported structure declarator.

Definitions and Theorems

Function: structdecl-formalp

(defun structdecl-formalp (structdecl)
 (declare (xargs :guard (structdeclp structdecl)))
 (declare (xargs :guard (structdecl-unambp structdecl)))
 (let ((__function__ 'structdecl-formalp))
  (declare (ignorable __function__))
  (structdecl-case
   structdecl
   :member
   (and
     (not structdecl.extension)
     (b* (((mv okp tyspecs)
           (check-spec/qual-list-all-typespec structdecl.specqual)))
       (and okp (type-spec-list-formalp tyspecs)))
     (consp structdecl.declor)
     (endp (cdr structdecl.declor))
     (structdeclor-formalp (car structdecl.declor))
     (endp structdecl.attrib))
   :statassert nil
   :empty nil)))

Theorem: booleanp-of-structdecl-formalp

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

Theorem: structdecl-formalp-of-structdecl-fix-structdecl

(defthm structdecl-formalp-of-structdecl-fix-structdecl
  (equal (structdecl-formalp (structdecl-fix structdecl))
         (structdecl-formalp structdecl)))

Theorem: structdecl-formalp-structdecl-equiv-congruence-on-structdecl

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