Major Section: ACL2-BUILT-INS
Example Forms: ; Returns the list (3 4): (mv-list 2 (mv 3 4)) ; Returns a list containing the three values returned by var-fn-count: (mv-list 3 (var-fn-count '(cons (binary-+ x y) z) nil)) General form: (mv-list n term)
Logically, (mv-list n term) is just term; that is, in the logic
mv-list simply returns its second argument. However, the evaluation of a
call of mv-list on explicit values always results in a single value,
which is a (null-terminated) list. For evaluation, the term n above (the
first argument to an mv-list call) must ``essentially'' (see below) be an
integer not less than 2, where that integer is the number of values returned
by the evaluation of term (the second argument to that mv-list call).
We say ``essentially'' above because it suffices that the translation of
n to a term (see trans) be of the form (quote k), where k is an
integer greater than 1. So for example, if term above returns three
values, then n can be the expression 3, or (quote 3), or even
(mac 3) if mac is a macro defined by (defmacro mac (x) x). But
n cannot be (+ 1 2), because even though that expression evaluates to
3, nevertheless it translates to (binary-+ '1 '2), not to
(quote 3).
Mv-list is the ACL2 analogue of the Common Lisp construct
multiple-value-list.
To see the ACL2 definition of this function, see pf.
