		Search-engine friendly clone of the ACL2 documentation.

Address

Svex-add-delay-top

Signature
(svex-add-delay-top x delay) → *
Arguments: x — Guard (svex-p x).; delay — Guard (natp delay).

Definitions and Theorems

Function: svex-add-delay-top

(defun svex-add-delay-top (x delay)
  (declare (xargs :guard (and (svex-p x) (natp delay))))
  (let ((__function__ 'svex-add-delay-top))
    (declare (ignorable __function__))
    (mbe :logic (svex-add-delay x delay)
         :exec
         (if (zp delay)
             x
           (svex-add-delay x delay)))))