### MV-LIST

converting multiple-valued result to a single-valued list
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.