returning a multiple value
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.