		Search-engine friendly clone of the ACL2 documentation.

Formalized-subset

Struct-declor-formalp

Check if a structure declarator has formal dynamic semantics.

Signature
(struct-declor-formalp structdeclor) → yes/no
Arguments: structdeclor — Guard (struct-declorp 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: struct-declor-formalp

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

Theorem: booleanp-of-struct-declor-formalp

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

Theorem: struct-declor-formalp-of-struct-declor-fix-structdeclor

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

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

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