		Search-engine friendly clone of the ACL2 documentation.

Type-checking

Funparam-to-var/const-sinfo

Turn a function parameter into static information about the parameter as a variable or constant.

Signature
(funparam-to-var/const-sinfo param) → info
Arguments: param — Guard (funparamp param).
Returns: info — Type (var/const-sinfop info).

For now we treat public and private parameters as just variables, and we treat constant and const parameters as just constants. We may extend this in the future.

Definitions and Theorems

Function: funparam-to-var/const-sinfo

(defun funparam-to-var/const-sinfo (param)
  (declare (xargs :guard (funparamp param)))
  (let ((__function__ 'funparam-to-var/const-sinfo))
    (declare (ignorable __function__))
    (b* (((funparam param) param)
         (constp (or (var/const-sort-case param.sort :constant)
                     (var/const-sort-case param.sort :const))))
      (make-var/const-sinfo :type param.type
                            :constp constp))))

Theorem: var/const-sinfop-of-funparam-to-var/const-sinfo

(defthm var/const-sinfop-of-funparam-to-var/const-sinfo
  (b* ((info (funparam-to-var/const-sinfo param)))
    (var/const-sinfop info))
  :rule-classes :rewrite)

Theorem: funparam-to-var/const-sinfo-of-funparam-fix-param

(defthm funparam-to-var/const-sinfo-of-funparam-fix-param
  (equal (funparam-to-var/const-sinfo (funparam-fix param))
         (funparam-to-var/const-sinfo param)))

Theorem: funparam-to-var/const-sinfo-funparam-equiv-congruence-on-param

(defthm
     funparam-to-var/const-sinfo-funparam-equiv-congruence-on-param
  (implies (funparam-equiv param param-equiv)
           (equal (funparam-to-var/const-sinfo param)
                  (funparam-to-var/const-sinfo param-equiv)))
  :rule-classes :congruence)