		Search-engine friendly clone of the ACL2 documentation.

Expr-gin

Make-expr-gin

Basic constructor macro for expr-gin structures.

Syntax

(make-expr-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 expr-gin structures. It simply conses together a structure with the specified fields.

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

Definition

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

Macro: make-expr-gin

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

Function: expr-gin

(defun expr-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__ 'expr-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)))))