returning multiple values
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.