(vl-left-associate-alternating-propexpr/op-list x) → propexpr
Function:
(defun vl-left-associate-alternating-propexpr/op-list (x) (declare (xargs :guard (vl-alternating-propexpr/op-list-p x))) (let ((__function__ 'vl-left-associate-alternating-propexpr/op-list)) (declare (ignorable __function__)) (if (atom (cdr x)) (vl-propexpr-fix (first x)) (b* (((list* left op right rest) x)) (vl-left-associate-alternating-propexpr/op-list (cons (make-vl-propbinary :left left :op op :right right) rest))))))
Theorem:
(defthm vl-propexpr-p-of-vl-left-associate-alternating-propexpr/op-list (b* ((propexpr (vl-left-associate-alternating-propexpr/op-list x))) (vl-propexpr-p propexpr)) :rule-classes :rewrite)