Major Section: ACL2-BUILT-INS
Mv is the mechanism provided by ACL2 for returning two or more values.
Logically, (mv x1 x2 ... xn) is the same as (list x1 x2 ... xn), a
list of the indicated values. However, ACL2 avoids the cost of building this
list structure, with the cost that mv may only be used in a certain style
in definitions: if a function ever returns using mv (either directly, or
by calling another function that returns a multiple value), then this
function must always return the same number of values.
For more explanation of the multiple value mechanism, see mv-let. Also see mv-list for a way to convert a multiple value into an ordinary list.
ACL2 does not support the Common Lisp construct values, whose logical
meaning seems difficult to characterize. Mv is the ACL2 analogue of that
construct.
