		Search-engine friendly clone of the ACL2 documentation.

Formalized-subset

Param-declon-list-formalp

Check if all the parameter declarations in a list have formal dynamic semantics.

Signature
(param-declon-list-formalp params) → yes/no
Arguments: params — Guard (param-declon-listp params).
Returns: yes/no — Type (booleanp yes/no).

Definitions and Theorems

Function: param-declon-list-formalp

(defun param-declon-list-formalp (params)
  (declare (xargs :guard (param-declon-listp params)))
  (declare (xargs :guard (param-declon-list-unambp params)))
  (let ((__function__ 'param-declon-list-formalp))
    (declare (ignorable __function__))
    (or (endp params)
        (and (param-declon-formalp (car params))
             (param-declon-list-formalp (cdr params))))))

Theorem: booleanp-of-param-declon-list-formalp

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

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

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

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

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