Extract the delay amount from a simple enough delay, if any.
(vl-edgesynth-simple-delay->amount x) → amount
Function:
(defun vl-edgesynth-simple-delay->amount (x) (declare (xargs :guard (and (vl-maybe-delayoreventcontrol-p x) (vl-edgesynth-simple-delay-p x)))) (let ((__function__ 'vl-edgesynth-simple-delay->amount)) (declare (ignorable __function__)) (and x (vl-resolved->val (vl-delaycontrol->value x)))))
Theorem:
(defthm maybe-natp-of-vl-edgesynth-simple-delay->amount (b* ((amount (vl-edgesynth-simple-delay->amount x))) (maybe-natp amount)) :rule-classes :type-prescription)