		Search-engine friendly clone of the ACL2 documentation.

Split-fn-implementation

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
        (make-param-declor-nonabstract
             :declor (add-pointer-declor param-declon.declor.declor)
             :info nil)
        :abstract (param-declor-fix param-declon.declor)
        :none (param-declor-fix param-declon.declor)
        :ambig (param-declor-fix param-declon.declor))
   :attribs param-declon.attribs)))

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)