(typed-variable-list->-expression-variable-list l) → r
Function:
(defun typed-variable-list->-expression-variable-list (l) (declare (xargs :guard (typed-variable-listp l))) (let ((__function__ 'typed-variable-list->-expression-variable-list)) (declare (ignorable __function__)) (if (endp l) nil (cons (make-expression-variable :name (typed-variable->name (car l))) (typed-variable-list->-expression-variable-list (cdr l))))))
Theorem:
(defthm expression-listp-of-typed-variable-list->-expression-variable-list (b* ((r (typed-variable-list->-expression-variable-list l))) (expression-listp r)) :rule-classes :rewrite)