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 and
l is a true-listp.
Mv-nth is equivalent to the Common Lisp function nth, 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)))
