		Search-engine friendly clone of the ACL2 documentation.

Svtv-probe

Make-svtv-probe

Basic constructor macro for svtv-probe structures.

Syntax

(make-svtv-probe [:signal <signal>] 
                 [:time <time>])

This is the usual way to construct svtv-probe structures. It simply conses together a structure with the specified fields.

This macro generates a new svtv-probe structure from scratch. See also change-svtv-probe, which can "change" an existing structure, instead.

Definition

This is an ordinary make- macro introduced by defprod.

Macro: make-svtv-probe

(defmacro make-svtv-probe (&rest args)
  (std::make-aggregate 'svtv-probe
                       args '((:signal) (:time))
                       'make-svtv-probe
                       nil))

Function: svtv-probe

(defun svtv-probe (signal time)
  (declare (xargs :guard (and (svar-p signal) (natp time))))
  (declare (xargs :guard t))
  (let ((__function__ 'svtv-probe))
    (declare (ignorable __function__))
    (b* ((signal (mbe :logic (svar-fix signal)
                      :exec signal))
         (time (mbe :logic (nfix time) :exec time)))
      (list (cons 'signal signal)
            (cons 'time time)))))