Remove the type annotations from a list of variables.
(atj-type-unannotate-vars vars) → unannotated-vars
The annotating types are discarded.
Function:
(defun atj-type-unannotate-vars (vars) (declare (xargs :guard (symbol-listp vars))) (let ((__function__ 'atj-type-unannotate-vars)) (declare (ignorable __function__)) (b* (((when (endp vars)) nil) ((mv var &) (atj-type-unannotate-var (car vars))) (vars (atj-type-unannotate-vars (cdr vars)))) (cons var vars))))
Theorem:
(defthm symbol-listp-of-atj-type-unannotate-vars (b* ((unannotated-vars (atj-type-unannotate-vars vars))) (symbol-listp unannotated-vars)) :rule-classes :rewrite)
Theorem:
(defthm len-of-atj-type-unannotate-vars (b* ((?unannotated-vars (atj-type-unannotate-vars vars))) (equal (len unannotated-vars) (len vars))))