		Search-engine friendly clone of the ACL2 documentation.

Lstmt-gout

Make-lstmt-gout

Basic constructor macro for lstmt-gout structures.

Syntax

(make-lstmt-gout [:stmt <stmt>] 
                 [:test-term <test-term>] 
                 [:body-term <body-term>] 
                 [:affect <affect>] 
                 [:limit-body <limit-body>] 
                 [:limit-all <limit-all>] 
                 [:events <events>] 
                 [:thm-name <thm-name>] 
                 [:thm-index <thm-index>] 
                 [:names-to-avoid <names-to-avoid>])

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

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

Definition

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

Macro: make-lstmt-gout

(defmacro make-lstmt-gout (&rest args)
  (std::make-aggregate 'lstmt-gout
                       args
                       '((:stmt)
                         (:test-term)
                         (:body-term)
                         (:affect)
                         (:limit-body)
                         (:limit-all)
                         (:events)
                         (:thm-name)
                         (:thm-index)
                         (:names-to-avoid))
                       'make-lstmt-gout
                       nil))

Function: lstmt-gout

(defun lstmt-gout (stmt test-term body-term
                        affect limit-body limit-all events
                        thm-name thm-index names-to-avoid)
 (declare (xargs :guard (and (stmtp stmt)
                             (pseudo-termp test-term)
                             (pseudo-termp body-term)
                             (symbol-listp affect)
                             (pseudo-termp limit-body)
                             (pseudo-termp limit-all)
                             (pseudo-event-form-listp events)
                             (symbolp thm-name)
                             (posp thm-index)
                             (symbol-listp names-to-avoid))))
 (declare (xargs :guard t))
 (let ((__function__ 'lstmt-gout))
  (declare (ignorable __function__))
  (b* ((stmt (mbe :logic (stmt-fix stmt) :exec stmt))
       (test-term (mbe :logic (pseudo-term-fix test-term)
                       :exec test-term))
       (body-term (mbe :logic (pseudo-term-fix body-term)
                       :exec body-term))
       (affect (mbe :logic (symbol-list-fix affect)
                    :exec affect))
       (limit-body (mbe :logic (pseudo-term-fix limit-body)
                        :exec limit-body))
       (limit-all (mbe :logic (pseudo-term-fix limit-all)
                       :exec limit-all))
       (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 (acl2::pos-fix thm-index)
                       :exec thm-index))
       (names-to-avoid (mbe :logic (symbol-list-fix names-to-avoid)
                            :exec names-to-avoid)))
    (list (cons 'stmt stmt)
          (cons 'test-term test-term)
          (cons 'body-term body-term)
          (cons 'affect affect)
          (cons 'limit-body limit-body)
          (cons 'limit-all limit-all)
          (cons 'events events)
          (cons 'thm-name thm-name)
          (cons 'thm-index thm-index)
          (cons 'names-to-avoid
                names-to-avoid)))))