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