		Search-engine friendly clone of the ACL2 documentation.

Split-fn

Add-pointer-param-declon

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

Definitions and Theorems

Function: add-pointer-param-declon

(defun add-pointer-param-declon (param-declon)
  (declare (xargs :guard (param-declonp param-declon)))
  (b* (((param-declon param-declon)
        param-declon))
    (make-param-declon
         :specs param-declon.specs
         :declor
         (param-declor-case
              param-declon.declor
              :nonabstract
              (param-declor-nonabstract
                   (add-pointer-declor param-declon.declor.declor))
              :abstract (param-declor-fix param-declon.declor)
              :none (param-declor-fix param-declon.declor)
              :ambig (param-declor-fix param-declon.declor)))))

Theorem: param-declonp-of-add-pointer-param-declon

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