		Search-engine friendly clone of the ACL2 documentation.

Gout

Make-gout

Basic constructor macro for gout structures.

Syntax

(make-gout [:events <events>] 
           [:thm-index <thm-index>] 
           [:thm-name <thm-name>] 
           [:vartys <vartys>])

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

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

Definition

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

Macro: make-gout

(defmacro make-gout (&rest args)
  (std::make-aggregate 'gout
                       args
                       '((:events)
                         (:thm-index)
                         (:thm-name)
                         (:vartys))
                       'make-gout
                       nil))

Function: gout

(defun gout (events thm-index thm-name vartys)
 (declare (xargs :guard (and (pseudo-event-form-listp events)
                             (posp thm-index)
                             (symbolp thm-name)
                             (c::ident-type-mapp vartys))))
 (declare (xargs :guard t))
 (let ((__function__ 'gout))
  (declare (ignorable __function__))
  (b* ((events (mbe :logic (acl2::pseudo-event-form-list-fix events)
                    :exec events))
       (thm-index (mbe :logic (pos-fix thm-index)
                       :exec thm-index))
       (thm-name (mbe :logic (acl2::symbol-fix thm-name)
                      :exec thm-name))
       (vartys (mbe :logic (c::ident-type-map-fix vartys)
                    :exec vartys)))
    (list (cons 'events events)
          (cons 'thm-index thm-index)
          (cons 'thm-name thm-name)
          (cons 'vartys vartys)))))