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