		Search-engine friendly clone of the ACL2 documentation.

Exprs-gin

Make-exprs-gin

Basic constructor macro for exprs-gin structures.

Syntax

(make-exprs-gin [:context <context>] 
                [:inscope <inscope>] 
                [:prec-tags <prec-tags>] 
                [:fn <fn>] 
                [:fn-guard <fn-guard>] 
                [:compst-var <compst-var>] 
                [:thm-index <thm-index>] 
                [:names-to-avoid <names-to-avoid>] 
                [:proofs <proofs>])

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

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

Definition

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

Macro: make-exprs-gin

(defmacro make-exprs-gin (&rest args)
  (std::make-aggregate 'exprs-gin
                       args
                       '((:context)
                         (:inscope)
                         (:prec-tags)
                         (:fn)
                         (:fn-guard)
                         (:compst-var)
                         (:thm-index)
                         (:names-to-avoid)
                         (:proofs))
                       'make-exprs-gin
                       nil))

Function: exprs-gin

(defun exprs-gin (context inscope prec-tags fn fn-guard compst-var
                          thm-index names-to-avoid proofs)
 (declare
      (xargs :guard (and (atc-contextp context)
                         (atc-symbol-varinfo-alist-listp inscope)
                         (atc-string-taginfo-alistp prec-tags)
                         (symbolp fn)
                         (symbolp fn-guard)
                         (symbolp compst-var)
                         (posp thm-index)
                         (symbol-listp names-to-avoid)
                         (booleanp proofs))))
 (declare (xargs :guard t))
 (let ((__function__ 'exprs-gin))
  (declare (ignorable __function__))
  (b*
   ((context (mbe :logic (atc-context-fix context)
                  :exec context))
    (inscope (mbe :logic (atc-symbol-varinfo-alist-list-fix inscope)
                  :exec inscope))
    (prec-tags (mbe :logic (atc-string-taginfo-alist-fix prec-tags)
                    :exec prec-tags))
    (fn (mbe :logic (symbol-fix fn) :exec fn))
    (fn-guard (mbe :logic (symbol-fix fn-guard)
                   :exec fn-guard))
    (compst-var (mbe :logic (symbol-fix compst-var)
                     :exec compst-var))
    (thm-index (mbe :logic (pos-fix thm-index)
                    :exec thm-index))
    (names-to-avoid (mbe :logic (symbol-list-fix names-to-avoid)
                         :exec names-to-avoid))
    (proofs (mbe :logic (acl2::bool-fix proofs)
                 :exec proofs)))
   (list (cons 'context context)
         (cons 'inscope inscope)
         (cons 'prec-tags prec-tags)
         (cons 'fn fn)
         (cons 'fn-guard fn-guard)
         (cons 'compst-var compst-var)
         (cons 'thm-index thm-index)
         (cons 'names-to-avoid names-to-avoid)
         (cons 'proofs proofs)))))