		Search-engine friendly clone of the ACL2 documentation.

Formalized-subset

Dirdeclor-block-formalp

Check if a direct declarator has formal dynamic semantics, as part of a block item declaration.

Signature
(dirdeclor-block-formalp dirdeclor) → yes/no
Arguments: dirdeclor — Guard (dirdeclorp dirdeclor).
Returns: yes/no — Type (booleanp yes/no).

In c::exec-block-item, the declaration case requires an object (not function) declarator that is not an array declarator. So we can only have an identifier.

Definitions and Theorems

Function: dirdeclor-block-formalp

(defun dirdeclor-block-formalp (dirdeclor)
  (declare (xargs :guard (dirdeclorp dirdeclor)))
  (declare (xargs :guard (dirdeclor-unambp dirdeclor)))
  (let ((__function__ 'dirdeclor-block-formalp))
    (declare (ignorable __function__))
    (and (dirdeclor-case dirdeclor :ident)
         (ident-formalp (dirdeclor-ident->ident dirdeclor)))))

Theorem: booleanp-of-dirdeclor-block-formalp

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

Theorem: dirdeclor-block-formalp-of-dirdeclor-fix-dirdeclor

(defthm dirdeclor-block-formalp-of-dirdeclor-fix-dirdeclor
  (equal (dirdeclor-block-formalp (dirdeclor-fix dirdeclor))
         (dirdeclor-block-formalp dirdeclor)))

Theorem: dirdeclor-block-formalp-dirdeclor-equiv-congruence-on-dirdeclor

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