		Search-engine friendly clone of the ACL2 documentation.

Parse-property

Vl-delay-se-tail-p

Temporary structure to support left-associative parsing of { cycle_delay_range repeat_se }.

Signature
(vl-delay-se-tail-p x) → *

Definitions and Theorems

Function: vl-delay-se-tail-p

(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: vl-delay-se-tail-p-when-atom

(defthm vl-delay-se-tail-p-when-atom
  (implies (atom x)
           (equal (vl-delay-se-tail-p x) (not x))))

Theorem: vl-delay-se-tail-p-of-list*

(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))))