		Search-engine friendly clone of the ACL2 documentation.

Formalized-subset

Structdeclor-formalp

Check if a structure declarator has formal dynamic semantics.

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

The declarator must be present and supported. The optional expression must be absent.

Definitions and Theorems

Function: structdeclor-formalp

(defun structdeclor-formalp (structdeclor)
  (declare (xargs :guard (structdeclorp structdeclor)))
  (declare (xargs :guard (structdeclor-unambp structdeclor)))
  (let ((__function__ 'structdeclor-formalp))
    (declare (ignorable __function__))
    (b* (((structdeclor structdeclor)
          structdeclor))
      (and structdeclor.declor?
           (declor-obj-formalp structdeclor.declor?)
           (not structdeclor.expr?)))))

Theorem: booleanp-of-structdeclor-formalp

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

Theorem: structdeclor-formalp-of-structdeclor-fix-structdeclor

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

Theorem: structdeclor-formalp-structdeclor-equiv-congruence-on-structdeclor

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