		Search-engine friendly clone of the ACL2 documentation.

Formalized-subset

Paramdecl-formalp

Check if a parameter declaration has formal dynamic semantics.

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

The declaration specifiers must be all type specifiers, and must form a supported type. The parameter declarator must be a supported one.

Definitions and Theorems

Function: paramdecl-formalp

(defun paramdecl-formalp (paramdecl)
  (declare (xargs :guard (paramdeclp paramdecl)))
  (declare (xargs :guard (paramdecl-unambp paramdecl)))
  (let ((__function__ 'paramdecl-formalp))
    (declare (ignorable __function__))
    (b* (((paramdecl paramdecl) paramdecl)
         ((mv okp tyspecs)
          (check-decl-spec-list-all-typespec paramdecl.spec)))
      (and okp (type-spec-list-formalp tyspecs)
           (paramdeclor-formalp paramdecl.decl)))))

Theorem: booleanp-of-paramdecl-formalp

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

Theorem: paramdecl-formalp-of-paramdecl-fix-paramdecl

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

Theorem: paramdecl-formalp-paramdecl-equiv-congruence-on-paramdecl

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