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 multiple values), then this function
must always return the same number of multiple 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.