### MV?

return one or more values
Major Section: ACL2-BUILT-INS

`Mv?`

is designed to work with `mv?-let`

, generalizing how `mv`

works
with `mv-let`

by allowing the binding of a single variable. For example,
the following form is legal.

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

The expression above is equivalent to the following expression, because
`(mv? form)`

expands to `form`

for any expression, `form`

.
(let ((y (f x)))
(declare (type integer y))
(g x y z))

Logically, `(mv? x)`

is the same as `x`

, while `(mv? v1 v2 ...)`

is the
same as `(list v1 v2 ...)`

. Also see mv and see mv?-let.