		Search-engine friendly clone of the ACL2 documentation.

Lstmt-gin

Make-lstmt-gin

Basic constructor macro for lstmt-gin structures.

Syntax

(make-lstmt-gin [:context <context>] 
                [:typed-formals <typed-formals>] 
                [:inscope <inscope>] 
                [:fn <fn>] 
                [:fn-guard <fn-guard>] 
                [:compst-var <compst-var>] 
                [:fenv-var <fenv-var>] 
                [:limit-var <limit-var>] 
                [:measure-for-fn <measure-for-fn>] 
                [:measure-formals <measure-formals>] 
                [:prec-fns <prec-fns>] 
                [:prec-tags <prec-tags>] 
                [:prec-objs <prec-objs>] 
                [:thm-index <thm-index>] 
                [:names-to-avoid <names-to-avoid>] 
                [:proofs <proofs>])

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

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

Definition

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

Macro: make-lstmt-gin

(defmacro make-lstmt-gin (&rest args)
  (std::make-aggregate 'lstmt-gin
                       args
                       '((:context)
                         (:typed-formals)
                         (:inscope)
                         (:fn)
                         (:fn-guard)
                         (:compst-var)
                         (:fenv-var)
                         (:limit-var)
                         (:measure-for-fn)
                         (:measure-formals)
                         (:prec-fns)
                         (:prec-tags)
                         (:prec-objs)
                         (:thm-index)
                         (:names-to-avoid)
                         (:proofs))
                       'make-lstmt-gin
                       nil))

Function: lstmt-gin

(defun lstmt-gin (context typed-formals
                          inscope fn fn-guard compst-var fenv-var
                          limit-var measure-for-fn measure-formals
                          prec-fns prec-tags prec-objs
                          thm-index names-to-avoid proofs)
 (declare
      (xargs :guard (and (atc-contextp context)
                         (atc-symbol-varinfo-alistp typed-formals)
                         (atc-symbol-varinfo-alist-listp inscope)
                         (symbolp fn)
                         (symbolp fn-guard)
                         (symbolp compst-var)
                         (symbolp fenv-var)
                         (symbolp limit-var)
                         (symbolp measure-for-fn)
                         (symbol-listp measure-formals)
                         (atc-symbol-fninfo-alistp prec-fns)
                         (atc-string-taginfo-alistp prec-tags)
                         (atc-string-objinfo-alistp prec-objs)
                         (posp thm-index)
                         (symbol-listp names-to-avoid)
                         (booleanp proofs))))
 (declare (xargs :guard t))
 (let ((__function__ 'lstmt-gin))
  (declare (ignorable __function__))
  (b*
   ((context (mbe :logic (atc-context-fix context)
                  :exec context))
    (typed-formals
         (mbe :logic (atc-symbol-varinfo-alist-fix typed-formals)
              :exec typed-formals))
    (inscope (mbe :logic (atc-symbol-varinfo-alist-list-fix inscope)
                  :exec inscope))
    (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))
    (fenv-var (mbe :logic (symbol-fix fenv-var)
                   :exec fenv-var))
    (limit-var (mbe :logic (symbol-fix limit-var)
                    :exec limit-var))
    (measure-for-fn (mbe :logic (symbol-fix measure-for-fn)
                         :exec measure-for-fn))
    (measure-formals (mbe :logic (symbol-list-fix measure-formals)
                          :exec measure-formals))
    (prec-fns (mbe :logic (atc-symbol-fninfo-alist-fix prec-fns)
                   :exec prec-fns))
    (prec-tags (mbe :logic (atc-string-taginfo-alist-fix prec-tags)
                    :exec prec-tags))
    (prec-objs (mbe :logic (atc-string-objinfo-alist-fix prec-objs)
                    :exec prec-objs))
    (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 'typed-formals typed-formals)
         (cons 'inscope inscope)
         (cons 'fn fn)
         (cons 'fn-guard fn-guard)
         (cons 'compst-var compst-var)
         (cons 'fenv-var fenv-var)
         (cons 'limit-var limit-var)
         (cons 'measure-for-fn measure-for-fn)
         (cons 'measure-formals measure-formals)
         (cons 'prec-fns prec-fns)
         (cons 'prec-tags prec-tags)
         (cons 'prec-objs prec-objs)
         (cons 'thm-index thm-index)
         (cons 'names-to-avoid names-to-avoid)
         (cons 'proofs proofs)))))