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