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.