Major Section: ACL2-BUILT-INS
(Mv-nth n l) is the nth element of l, zero-based. If n is
greater than or equal to the length of l, then mv-nth returns
nil.
(Mv-nth n l) has a guard that n is a non-negative integer.
Mv-nth is equivalent to the Common Lisp function nth (although
without the guard condition that the list is a true-listp), but is used
by ACL2 to access the nth value returned by a multiply valued expression.
For example, the following are logically equivalent:
(mv-let (erp val state)
(read-object ch state)
(value (list erp val)))
and
(let ((erp (mv-nth 0 (read-object ch state)))
(val (mv-nth 1 (read-object ch state)))
(state (mv-nth 2 (read-object ch state))))
(value (list erp val)))
To see the ACL2 definition of mv-nth, see pf.
If EXPR is an expression that is multiply valued, then the form
(mv-nth n EXPR) is illegal both in definitions and in forms submitted
directly to the ACL2 loop. Indeed, EXPR cannot be passed as an argument
to any function (mv-nth or otherwise) in such an evaluation context. The
reason is that ACL2 code compiled for execution does not actually create a
list for multiple value return; for example, the read-object call above
logically returns a list of length 3, but when evaluated, it instead stores
its three returned values without constructing a list. In such cases you can
use mv-nth to access the corresponding list by using mv-list, writing
(mv-nth n (mv-list k EXPR)) for suitable k, where mv-list
converts a multiple value result into the corresponding list;
see mv-list.
