Mv-list
Converting multiple-value result to a single-value list
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 (nil-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.
Function: mv-list
(defun mv-list (input-arity x)
(declare (xargs :guard t)
(ignore input-arity))
x)
