		Search-engine friendly clone of the ACL2 documentation.

Pexprs-gout

Make-pexprs-gout

Basic constructor macro for pexprs-gout structures.

Syntax

(make-pexprs-gout [:exprs <exprs>] 
                  [:types <types>] 
                  [:terms <terms>] 
                  [:events <events>] 
                  [:thm-names <thm-names>] 
                  [:thm-index <thm-index>] 
                  [:names-to-avoid <names-to-avoid>])

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

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

Definition

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

Macro: make-pexprs-gout

(defmacro make-pexprs-gout (&rest args)
  (std::make-aggregate 'pexprs-gout
                       args
                       '((:exprs)
                         (:types)
                         (:terms)
                         (:events)
                         (:thm-names)
                         (:thm-index)
                         (:names-to-avoid))
                       'make-pexprs-gout
                       nil))

Function: pexprs-gout

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