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