		Search-engine friendly clone of the ACL2 documentation.

Formalized-subset

Param-declon-formalp

Check if a parameter declaration has formal dynamic semantics.

Signature
(param-declon-formalp param) → yes/no
Arguments: param — Guard (param-declonp param).
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. There must be no ending attribute specifiers.

Definitions and Theorems

Function: param-declon-formalp

(defun param-declon-formalp (param)
  (declare (xargs :guard (param-declonp param)))
  (declare (xargs :guard (param-declon-unambp param)))
  (let ((__function__ 'param-declon-formalp))
    (declare (ignorable __function__))
    (b* (((param-declon param) param)
         ((mv okp tyspecs)
          (check-decl-spec-list-all-typespec param.specs)))
      (and okp (type-spec-list-formalp tyspecs)
           (param-declor-formalp param.declor)
           (endp param.attribs)))))

Theorem: booleanp-of-param-declon-formalp

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

Theorem: param-declon-formalp-of-param-declon-fix-param

(defthm param-declon-formalp-of-param-declon-fix-param
  (equal (param-declon-formalp (param-declon-fix param))
         (param-declon-formalp param)))

Theorem: param-declon-formalp-param-declon-equiv-congruence-on-param

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