		Search-engine friendly clone of the ACL2 documentation.

Expr-gout

Make-expr-gout

Basic constructor macro for expr-gout structures.

Syntax

(make-expr-gout [:expr <expr>] 
                [:type <type>] 
                [:term <term>] 
                [:events <events>] 
                [:thm-name <thm-name>] 
                [:thm-index <thm-index>] 
                [:names-to-avoid <names-to-avoid>])

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

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

Definition

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

Macro: make-expr-gout

(defmacro make-expr-gout (&rest args)
  (std::make-aggregate 'expr-gout
                       args
                       '((:expr)
                         (:type)
                         (:term)
                         (:events)
                         (:thm-name)
                         (:thm-index)
                         (:names-to-avoid))
                       'make-expr-gout
                       nil))

Function: expr-gout

(defun expr-gout (expr type term events
                       thm-name thm-index names-to-avoid)
 (declare (xargs :guard (and (exprp expr)
                             (typep type)
                             (pseudo-termp term)
                             (pseudo-event-form-listp events)
                             (symbolp thm-name)
                             (posp thm-index)
                             (symbol-listp names-to-avoid))))
 (declare (xargs :guard t))
 (let ((__function__ 'expr-gout))
  (declare (ignorable __function__))
  (b* ((expr (mbe :logic (expr-fix expr) :exec expr))
       (type (mbe :logic (type-fix type) :exec type))
       (term (mbe :logic (pseudo-term-fix term)
                  :exec term))
       (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 'expr expr)
          (cons 'type type)
          (cons 'term term)
          (cons 'events events)
          (cons 'thm-name thm-name)
          (cons 'thm-index thm-index)
          (cons 'names-to-avoid
                names-to-avoid)))))