		Search-engine friendly clone of the ACL2 documentation.

Formalized-subset

Strunispec-formalp

Check if a structure declaration has formal dynamic semantics.

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

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

Definitions and Theorems

Function: strunispec-formalp

(defun strunispec-formalp (strunispec)
  (declare (xargs :guard (strunispecp strunispec)))
  (declare (xargs :guard (strunispec-unambp strunispec)))
  (let ((__function__ 'strunispec-formalp))
    (declare (ignorable __function__))
    (b* (((strunispec strunispec) strunispec))
      (and strunispec.name
           (ident-formalp strunispec.name)
           (structdecl-list-formalp strunispec.members)))))

Theorem: booleanp-of-strunispec-formalp

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

Theorem: strunispec-formalp-of-strunispec-fix-strunispec

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

Theorem: strunispec-formalp-strunispec-equiv-congruence-on-strunispec

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