		Search-engine friendly clone of the ACL2 documentation.

Formalized-subset

Struni-spec-formalp

Check if a structure declaration has formal dynamic semantics.

Signature
(struni-spec-formalp struni-spec) → yes/no
Arguments: struni-spec — Guard (struni-specp struni-spec).
Returns: yes/no — Type (booleanp yes/no).

The name must be present, and each structure declaration must be supported.

Definitions and Theorems

Function: struni-spec-formalp

(defun struni-spec-formalp (struni-spec)
  (declare (xargs :guard (struni-specp struni-spec)))
  (declare (xargs :guard (struni-spec-unambp struni-spec)))
  (let ((__function__ 'struni-spec-formalp))
    (declare (ignorable __function__))
    (b* (((struni-spec struni-spec) struni-spec))
      (and struni-spec.name?
           (ident-formalp struni-spec.name?)
           (structdecl-list-formalp struni-spec.members)))))

Theorem: booleanp-of-struni-spec-formalp

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

Theorem: struni-spec-formalp-of-struni-spec-fix-struni-spec

(defthm struni-spec-formalp-of-struni-spec-fix-struni-spec
  (equal (struni-spec-formalp (struni-spec-fix struni-spec))
         (struni-spec-formalp struni-spec)))

Theorem: struni-spec-formalp-struni-spec-equiv-congruence-on-struni-spec

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