Mv
Returning a multiple value
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.
Subtopics
- Mv-let
- Calling multi-valued ACL2 functions
- Mv-nth
- The mv-nth element (zero-based) of a list
- Mv-list
- Converting multiple-value result to a single-value list
- Mv?-let
- Calling possibly multi-valued ACL2 functions
- Mv?
- Return one or more values
