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