(vl-left-associate-delay-se-tail head tail) → propexpr
Function:
(defun vl-left-associate-delay-se-tail (head tail) (declare (xargs :guard (and (vl-propexpr-p head) (vl-delay-se-tail-p tail)))) (let ((__function__ 'vl-left-associate-delay-se-tail)) (declare (ignorable __function__)) (b* (((when (atom tail)) (vl-propexpr-fix head)) ((list* delay expr rest) tail) (new-head (make-vl-propthen :left head :delay delay :right expr))) (vl-left-associate-delay-se-tail new-head rest))))
Theorem:
(defthm vl-propexpr-p-of-vl-left-associate-delay-se-tail (b* ((propexpr (vl-left-associate-delay-se-tail head tail))) (vl-propexpr-p propexpr)) :rule-classes :rewrite)