Temporary structure to support left-associative parsing of
(vl-delay-se-tail-p x) → *
Function:
(defun vl-delay-se-tail-p (x) (declare (xargs :guard t)) (let ((__function__ 'vl-delay-se-tail-p)) (declare (ignorable __function__)) (if (atom x) (not x) (and (consp x) (consp (cdr x)) (and (vl-range-p (first x)) (vl-propexpr-p (second x)) (vl-delay-se-tail-p (cddr x)))))))
Theorem:
(defthm vl-delay-se-tail-p-when-atom (implies (atom x) (equal (vl-delay-se-tail-p x) (not x))))
Theorem:
(defthm vl-delay-se-tail-p-of-list* (equal (vl-delay-se-tail-p (list* delay expr rest)) (and (vl-range-p delay) (vl-propexpr-p expr) (vl-delay-se-tail-p rest))))