MV-NTH

the mv-nth element (zero-based) of a list
Major Section:  PROGRAMMING

(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 an example of the use of mv-nth, try

ACL2 !>:trans1 (mv-let (erp val state)
                       (read-object ch state)
                       (value (list erp val)))