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?.
