		Search-engine friendly clone of the ACL2 documentation.

Edgesynth

Vl-edgesynth-delays-okp

Check that internal delays on assignments are simple enough to process and compatible with one another.

Signature
(vl-edgesynth-delays-okp x) → okp
Arguments: x — Guard (vl-assigncontrols-p x).
Returns: okp — Type (booleanp okp).

Definitions and Theorems

Function: vl-edgesynth-delays-okp

(defun vl-edgesynth-delays-okp (x)
 (declare (xargs :guard (vl-assigncontrols-p x)))
 (let ((__function__ 'vl-edgesynth-delays-okp))
  (declare (ignorable __function__))
  (and
      (consp x)
      (vl-edgesynth-simple-delays-p x)
      (all-equalp (vl-edgesynth-simple-delay->amount (first x))
                  (vl-edgesynth-simple-delays->amounts (rest x))))))

Theorem: booleanp-of-vl-edgesynth-delays-okp

(defthm booleanp-of-vl-edgesynth-delays-okp
  (b* ((okp (vl-edgesynth-delays-okp x)))
    (booleanp okp))
  :rule-classes :type-prescription)

Theorem: vl-edgesynth-simple-delays-p-when-vl-edgesynth-delays-okp

(defthm vl-edgesynth-simple-delays-p-when-vl-edgesynth-delays-okp
  (implies (vl-edgesynth-delays-okp x)
           (vl-edgesynth-simple-delays-p x)))

Theorem: consp-when-vl-edgesynth-delays-okp

(defthm consp-when-vl-edgesynth-delays-okp
  (implies (vl-edgesynth-delays-okp x)
           (consp x))
  :rule-classes :compound-recognizer)

Subtopics

Vl-edgesynth-simple-delays->amounts: (vl-edgesynth-simple-delays->amounts x) maps vl-edgesynth-simple-delay->amount across a list.
Vl-edgesynth-simple-delays-p: (vl-edgesynth-simple-delays-p x) recognizes lists where every element satisfies vl-edgesynth-simple-delay-p.
Vl-edgesynth-simple-delay->amount: Extract the delay amount from a simple enough delay, if any.
Vl-edgesynth-simple-delay-p: Recognizer for empty delays and simple integer delays like #5.