		Search-engine friendly clone of the ACL2 documentation.

Split-fn-implementation

Map-add-pointer-param-declon

Signature
(map-add-pointer-param-declon param-declons) → param-declons$
Arguments: param-declons — Guard (param-declon-listp param-declons).
Returns: param-declons$ — Type (param-declon-listp param-declons$).

Definitions and Theorems

Function: map-add-pointer-param-declon

(defun map-add-pointer-param-declon (param-declons)
  (declare (xargs :guard (param-declon-listp param-declons)))
  (if (endp param-declons)
      nil
    (cons (add-pointer-param-declon (first param-declons))
          (map-add-pointer-param-declon (rest param-declons)))))

Theorem: param-declon-listp-of-map-add-pointer-param-declon

(defthm param-declon-listp-of-map-add-pointer-param-declon
 (b* ((param-declons$ (map-add-pointer-param-declon param-declons)))
   (param-declon-listp param-declons$))
 :rule-classes :rewrite)