		Search-engine friendly clone of the ACL2 documentation.

Formalized-subset

Dirdeclor-fun-formalp

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

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

It must be a function declarator with parameters, where the inner declarator is just a name; see ldm-dirdeclor-fun. The parameter declarations must be supported.

Definitions and Theorems

Function: dirdeclor-fun-formalp

(defun dirdeclor-fun-formalp (dirdeclor)
 (declare (xargs :guard (dirdeclorp dirdeclor)))
 (declare (xargs :guard (dirdeclor-unambp dirdeclor)))
 (let ((__function__ 'dirdeclor-fun-formalp))
  (declare (ignorable __function__))
  (dirdeclor-case
      dirdeclor
      :function-params
      (and (dirdeclor-case dirdeclor.declor :ident)
           (ident-formalp (dirdeclor-ident->ident dirdeclor.declor))
           (param-declon-list-formalp dirdeclor.params))
      :function-names
      (and (dirdeclor-case dirdeclor.declor :ident)
           (ident-formalp (dirdeclor-ident->ident dirdeclor.declor))
           (endp dirdeclor.names))
      :otherwise nil)))

Theorem: booleanp-of-dirdeclor-fun-formalp

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

Theorem: dirdeclor-fun-formalp-of-dirdeclor-fix-dirdeclor

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

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

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