		Search-engine friendly clone of the ACL2 documentation.

Ex-outs

Make-ex-outs

Basic constructor macro for ex-outs structures.

Syntax

(make-ex-outs [:expanded-term-lst <expanded-term-lst>] 
              [:expanded-fn-lst <expanded-fn-lst>])

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

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

Definition

This is an ordinary make- macro introduced by defprod.

Macro: make-ex-outs

(defmacro make-ex-outs (&rest args)
  (std::make-aggregate 'ex-outs
                       args
                       '((:expanded-term-lst)
                         (:expanded-fn-lst))
                       'make-ex-outs
                       nil))

Function: ex-outs

(defun ex-outs (expanded-term-lst expanded-fn-lst)
 (declare (xargs :guard (and (pseudo-term-listp expanded-term-lst)
                             (pseudo-term-alistp expanded-fn-lst))))
 (declare (xargs :guard t))
 (let ((acl2::__function__ 'ex-outs))
   (declare (ignorable acl2::__function__))
   (b* ((expanded-term-lst
             (mbe :logic (pseudo-term-list-fix expanded-term-lst)
                  :exec expanded-term-lst))
        (expanded-fn-lst
             (mbe :logic (pseudo-term-alist-fix expanded-fn-lst)
                  :exec expanded-fn-lst)))
     (list (cons 'expanded-term-lst
                 expanded-term-lst)
           (cons 'expanded-fn-lst
                 expanded-fn-lst)))))