(typed-variable-list->-expression l) → r
Function:
(defun typed-variable-list->-expression (l) (declare (xargs :guard (typed-variable-listp l))) (let ((__function__ 'typed-variable-list->-expression)) (declare (ignorable __function__)) (let ((exprs (typed-variable-list->-expression-variable-list l))) (if (equal (len exprs) 1) (car exprs) (make-expression-multi :arguments exprs)))))
Theorem:
(defthm expressionp-of-typed-variable-list->-expression (b* ((r (typed-variable-list->-expression l))) (expressionp r)) :rule-classes :rewrite)