Check a list of parameter declarations.
(check-param-declon-list params vartab tagenv) → new-vartab
We go through each element of the list, calling check-param-declon and threading the variable table through.
Function:
(defun check-param-declon-list (params vartab tagenv) (declare (xargs :guard (and (param-declon-listp params) (var-tablep vartab) (tag-envp tagenv)))) (let ((__function__ 'check-param-declon-list)) (declare (ignorable __function__)) (b* (((when (endp params)) (var-table-fix vartab)) ((okf vartab) (check-param-declon (car params) vartab tagenv))) (check-param-declon-list (cdr params) vartab tagenv))))
Theorem:
(defthm var-table-resultp-of-check-param-declon-list (b* ((new-vartab (check-param-declon-list params vartab tagenv))) (var-table-resultp new-vartab)) :rule-classes :rewrite)
Theorem:
(defthm check-param-declon-list-of-param-declon-list-fix-params (equal (check-param-declon-list (param-declon-list-fix params) vartab tagenv) (check-param-declon-list params vartab tagenv)))
Theorem:
(defthm check-param-declon-list-param-declon-list-equiv-congruence-on-params (implies (param-declon-list-equiv params params-equiv) (equal (check-param-declon-list params vartab tagenv) (check-param-declon-list params-equiv vartab tagenv))) :rule-classes :congruence)
Theorem:
(defthm check-param-declon-list-of-var-table-fix-vartab (equal (check-param-declon-list params (var-table-fix vartab) tagenv) (check-param-declon-list params vartab tagenv)))
Theorem:
(defthm check-param-declon-list-var-table-equiv-congruence-on-vartab (implies (var-table-equiv vartab vartab-equiv) (equal (check-param-declon-list params vartab tagenv) (check-param-declon-list params vartab-equiv tagenv))) :rule-classes :congruence)
Theorem:
(defthm check-param-declon-list-of-tag-env-fix-tagenv (equal (check-param-declon-list params vartab (tag-env-fix tagenv)) (check-param-declon-list params vartab tagenv)))
Theorem:
(defthm check-param-declon-list-tag-env-equiv-congruence-on-tagenv (implies (tag-env-equiv tagenv tagenv-equiv) (equal (check-param-declon-list params vartab tagenv) (check-param-declon-list params vartab tagenv-equiv))) :rule-classes :congruence)