		Search-engine friendly clone of the ACL2 documentation.

Simpadd0-gout

Make-simpadd0-gout

Basic constructor macro for simpadd0-gout structures.

Syntax

(make-simpadd0-gout [:events <events>] 
                    [:thm-name <thm-name>] 
                    [:thm-index <thm-index>] 
                    [:names-to-avoid <names-to-avoid>] 
                    [:vartys <vartys>] 
                    [:diffp <diffp>])

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

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

Definition

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

Macro: make-simpadd0-gout

(defmacro make-simpadd0-gout (&rest args)
  (std::make-aggregate 'simpadd0-gout
                       args
                       '((:events)
                         (:thm-name)
                         (:thm-index)
                         (:names-to-avoid)
                         (:vartys)
                         (:diffp))
                       'make-simpadd0-gout
                       nil))

Function: simpadd0-gout

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