Major Section: ACL2-BUILT-INS

`(Mv-nth n l)`

is the `n`

th 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.