		Search-engine friendly clone of the ACL2 documentation.

Vl-simpledelay-p

Vl-simpledelay->amount

Get the number of ticks for a simple delay.

Signature
(vl-simpledelay->amount x) → amount
Arguments: x — Guard (and (vl-gatedelay-p x) (vl-simpledelay-p x)).
Returns: amount — Type (natp amount).

Definitions and Theorems

Function: vl-simpledelay->amount

(defun vl-simpledelay->amount (x)
  (declare (xargs :guard (and (vl-gatedelay-p x)
                              (vl-simpledelay-p x))))
  (let ((__function__ 'vl-simpledelay->amount))
    (declare (ignorable __function__))
    (lnfix (vl-resolved->val (vl-gatedelay->rise x)))))

Theorem: natp-of-vl-simpledelay->amount

(defthm natp-of-vl-simpledelay->amount
  (b* ((amount (vl-simpledelay->amount x)))
    (natp amount))
  :rule-classes :type-prescription)