Basic constructor macro for svtv*-input structures.
(make-svtv*-input [:setting <setting>] [:toggle <toggle>] [:hold <hold>])
This is the usual way to construct svtv*-input structures. It simply conses together a structure with the specified fields.
This macro generates a new svtv*-input structure from scratch. See also change-svtv*-input, which can "change" an existing structure, instead.
This is an ordinary
Macro:
(defmacro make-svtv*-input (&rest args) (std::make-aggregate 'svtv*-input args '((:setting) (:toggle) (:hold . 1)) 'make-svtv*-input nil))
Function:
(defun svtv*-input (setting toggle hold) (declare (xargs :guard (and (svtv-entry-p setting) (maybe-posp toggle) (natp hold)))) (declare (xargs :guard t)) (let ((__function__ 'svtv*-input)) (declare (ignorable __function__)) (b* ((setting (mbe :logic (svtv-entry-fix setting) :exec setting)) (toggle (mbe :logic (acl2::maybe-posp-fix toggle) :exec toggle)) (hold (mbe :logic (nfix hold) :exec hold))) (list setting toggle hold))))