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.  