Major Section: PROGRAMMING
(Mv-nth n l) is the
nth element of
l, zero-based. If
greater than or equal to the length of
(Mv-nth n l) has a guard that
n is a non-negative integer.
Mv-nth is equivalent to the Common Lisp function
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
ACL2 !>:trans1 (mv-let (erp val state) (read-object ch state) (value (list erp val)))