		Search-engine friendly clone of the ACL2 documentation.

Formalized-subset

Struct-declon-formalp

Check if a structure declaration has formal dynamic semantics.

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

(defun struct-declon-formalp (structdeclon)
 (declare (xargs :guard (struct-declonp structdeclon)))
 (declare (xargs :guard (struct-declon-unambp structdeclon)))
 (let ((__function__ 'struct-declon-formalp))
  (declare (ignorable __function__))
  (struct-declon-case
   structdeclon
   :member
   (and
     (not structdeclon.extension)
     (b*
      (((mv okp tyspecs)
        (check-spec/qual-list-all-typespec structdeclon.specquals)))
      (and okp (type-spec-list-formalp tyspecs)))
     (consp structdeclon.declors)
     (endp (cdr structdeclon.declors))
     (struct-declor-formalp (car structdeclon.declors))
     (endp structdeclon.attribs))
   :statassert nil
   :empty nil)))

Theorem: booleanp-of-struct-declon-formalp

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

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

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

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

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