MV-NTH

the mv-nth element (zero-based) of a list
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.