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