		Search-engine friendly clone of the ACL2 documentation.

G-map

Make-g-map

Basic constructor macro for g-map structures.

Syntax

(make-g-map [:tag <tag>] 
            [:alist <alist>])

This is the usual way to construct g-map structures. It simply conses together a structure with the specified fields.

This macro generates a new g-map structure from scratch. See also change-g-map, which can "change" an existing structure, instead.

Definition

This is an ordinary make- macro introduced by defprod.

Macro: make-g-map

(defmacro make-g-map (&rest args)
  (std::make-aggregate 'g-map
                       args '((:tag) (:alist))
                       'make-g-map
                       nil))

Function: g-map

(defun g-map (tag alist)
  (declare (xargs :guard (and (g-map-tag-p tag)
                              (fgl-object-alist-p alist))))
  (declare (xargs :guard t))
  (let ((__function__ 'g-map))
    (declare (ignorable __function__))
    (b* ((tag (mbe :logic (g-map-tag-fix tag)
                   :exec tag))
         (alist (mbe :logic (fgl-object-alist-fix alist)
                     :exec alist)))
      (cons tag alist))))