Annotate each of a list of ACL2 variable with a corresponding singleton list of types.
(atj-type-annotate-vars vars types) → new-vars
Function:
(defun atj-type-annotate-vars (vars types) (declare (xargs :guard (and (symbol-listp vars) (atj-type-listp types)))) (declare (xargs :guard (int= (len vars) (len types)))) (let ((__function__ 'atj-type-annotate-vars)) (declare (ignorable __function__)) (cond ((endp vars) nil) (t (cons (atj-type-annotate-var (car vars) (list (car types))) (atj-type-annotate-vars (cdr vars) (cdr types)))))))
Theorem:
(defthm symbol-listp-of-atj-type-annotate-vars (b* ((new-vars (atj-type-annotate-vars vars types))) (symbol-listp new-vars)) :rule-classes :rewrite)
Theorem:
(defthm len-of-atj-type-annotate-vars (b* ((?new-vars (atj-type-annotate-vars vars types))) (equal (len new-vars) (len vars))))