### MV?-LET

calling possibly multi-valued ACL2 functions
Major Section: ACL2-BUILT-INS

`Mv?-let`

is a macro that extends the macro `mv-let`

by allowing a
single variable to be bound. Thus, the syntax is the same as that of
`mv-let`

except that `mv?-let`

is permitted to bind a single variable
to a form that produces a single value. The macros `mv?-let`

and `mv?`

are provided to facilitate the writing of macros that traffic in expressions
that could return one or more (multiple) values.

For example, the form

(mv?-let (y)
(f x)
(declare (type integer y))
(g x y z))

is equivalent to the following form.
(let ((y (f x)))
(declare (type integer y))
(g x y z))

Calls of `mv?-let`

and of `mv-let`

are equivalent when the first
argument contains at least two variables; see mv-let for documentation. In
the case of binding a single variable, the general form is

(mv?-let (var)
term
(declare ...) ... (declare ...)
body)

and this is equivalent to the following form (see let).
(let ((var term))
(declare ...) ... (declare ...)
body)

Also see mv?.