values, whose
logical meaning seems difficult to characterize. Mv is the ACL2
analogue of that construct.
Major Section: PROGRAMMING
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 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 values, whose
logical meaning seems difficult to characterize. Mv is the ACL2
analogue of that construct.