(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-binary :op op :left e1 :right e2 :atts atts) rest))) (vl-expr-fix (car x)))))
Theorem:
(defthm vl-expr-p-of-vl-left-associate-mixed-binop-list (b* ((expr (vl-left-associate-mixed-binop-list x))) (vl-expr-p expr)) :rule-classes :rewrite)