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