(vl-left-associate-mixed-binop-list x) → expr
Function:
(defun vl-left-associate-mixed-binop-list (x) (declare (xargs :guard (vl-mixed-binop-list-p x))) (let ((__function__ 'vl-left-associate-mixed-binop-list)) (declare (ignorable __function__)) (if (consp (cdr x)) (let ((e1 (first x)) (op (second x)) (atts (third x)) (e2 (fourth x)) (rest (cddddr x))) (vl-left-associate-mixed-binop-list (cons (make-vl-nonatom :op op :atts atts :args (list e1 e2)) rest))) (car x))))
Theorem:
(defthm vl-expr-p-of-vl-left-associate-mixed-binop-list (implies (and (vl-mixed-binop-list-p x)) (b* ((expr (vl-left-associate-mixed-binop-list x))) (vl-expr-p expr))) :rule-classes :rewrite)