Temporary structure to support parsing left-associative sequence expressions.
(vl-alternating-propexpr/op-list-p x) → *
Function:
(defun vl-alternating-propexpr/op-list-p (x) (declare (xargs :guard t)) (let ((__function__ 'vl-alternating-propexpr/op-list-p)) (declare (ignorable __function__)) (and (consp x) (vl-propexpr-p (first x)) (or (not (consp (cdr x))) (and (consp (cddr x)) (let ((op (second x)) (rest (cddr x))) (and (vl-property-binaryop-p op) (vl-alternating-propexpr/op-list-p rest))))))))
Theorem:
(defthm vl-alternating-propexpr/op-list-p-when-atom (implies (atom x) (equal (vl-alternating-propexpr/op-list-p x) nil)))
Theorem:
(defthm vl-alternating-propexpr/op-list-p-of-singleton (equal (vl-alternating-propexpr/op-list-p (list x)) (vl-propexpr-p x)))
Theorem:
(defthm vl-alternating-propexpr/op-list-p-of-list* (equal (vl-alternating-propexpr/op-list-p (list* x y z)) (and (vl-propexpr-p x) (vl-property-binaryop-p y) (vl-alternating-propexpr/op-list-p z))))