		Search-engine friendly clone of the ACL2 documentation.

Make-gin

Basic constructor macro for gin structures.

Syntax

(make-gin [:ienv <ienv>] 
          [:const-new <const-new>] 
          [:vartys <vartys>] 
          [:events <events>] 
          [:thm-index <thm-index>])

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

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

Definition

This is an ordinary make- macro introduced by fty::defprod.

Macro: make-gin

(defmacro make-gin (&rest args)
  (std::make-aggregate 'gin
                       args
                       '((:ienv)
                         (:const-new)
                         (:vartys)
                         (:events)
                         (:thm-index))
                       'make-gin
                       nil))

Function: gin

(defun gin (ienv const-new vartys events thm-index)
 (declare (xargs :guard (and (c$::ienvp ienv)
                             (symbolp const-new)
                             (c::ident-type-mapp vartys)
                             (pseudo-event-form-listp events)
                             (posp thm-index))))
 (declare (xargs :guard t))
 (let ((__function__ 'gin))
  (declare (ignorable __function__))
  (b* ((ienv (mbe :logic (c$::ienv-fix ienv)
                  :exec ienv))
       (const-new (mbe :logic (acl2::symbol-fix const-new)
                       :exec const-new))
       (vartys (mbe :logic (c::ident-type-map-fix vartys)
                    :exec vartys))
       (events (mbe :logic (acl2::pseudo-event-form-list-fix events)
                    :exec events))
       (thm-index (mbe :logic (pos-fix thm-index)
                       :exec thm-index)))
    (list (cons 'ienv ienv)
          (cons 'const-new const-new)
          (cons 'vartys vartys)
          (cons 'events events)
          (cons 'thm-index thm-index)))))