Major Section: PROGRAMMING
Mv is the mechanism provided by ACL2 for returning two or more
(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
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.
ACL2 does not support the Common Lisp construct
logical meaning seems difficult to characterize.
Mv is the ACL2
analogue of that construct.