		Search-engine friendly clone of the ACL2 documentation.

Stmt-gout

Make-stmt-gout

Basic constructor macro for stmt-gout structures.

Syntax

(make-stmt-gout [:items <items>] 
                [:type <type>] 
                [:term <term>] 
                [:context <context>] 
                [:inscope <inscope>] 
                [:limit <limit>] 
                [:events <events>] 
                [:thm-name <thm-name>] 
                [:thm-index <thm-index>] 
                [:names-to-avoid <names-to-avoid>])

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

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

Definition

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

Macro: make-stmt-gout

(defmacro make-stmt-gout (&rest args)
  (std::make-aggregate 'stmt-gout
                       args
                       '((:items)
                         (:type)
                         (:term)
                         (:context)
                         (:inscope)
                         (:limit)
                         (:events)
                         (:thm-name)
                         (:thm-index)
                         (:names-to-avoid))
                       'make-stmt-gout
                       nil))

Function: stmt-gout

(defun stmt-gout (items type term context inscope limit events
                        thm-name thm-index names-to-avoid)
 (declare
      (xargs :guard (and (block-item-listp items)
                         (typep type)
                         (pseudo-termp term)
                         (atc-contextp context)
                         (atc-symbol-varinfo-alist-listp inscope)
                         (pseudo-termp limit)
                         (pseudo-event-form-listp events)
                         (symbolp thm-name)
                         (posp thm-index)
                         (symbol-listp names-to-avoid))))
 (declare (xargs :guard t))
 (let ((__function__ 'stmt-gout))
  (declare (ignorable __function__))
  (b*
   ((items (mbe :logic (block-item-list-fix items)
                :exec items))
    (type (mbe :logic (type-fix type) :exec type))
    (term (mbe :logic (pseudo-term-fix term)
               :exec term))
    (context (mbe :logic (atc-context-fix context)
                  :exec context))
    (inscope (mbe :logic (atc-symbol-varinfo-alist-list-fix inscope)
                  :exec inscope))
    (limit (mbe :logic (pseudo-term-fix limit)
                :exec limit))
    (events (mbe :logic (acl2::pseudo-event-form-list-fix events)
                 :exec events))
    (thm-name (mbe :logic (symbol-fix thm-name)
                   :exec thm-name))
    (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)))
   (list (cons 'items items)
         (cons 'type type)
         (cons 'term term)
         (cons 'context context)
         (cons 'inscope inscope)
         (cons 'limit limit)
         (cons 'events events)
         (cons 'thm-name thm-name)
         (cons 'thm-index thm-index)
         (cons 'names-to-avoid
               names-to-avoid)))))