Mv?-let
Calling possibly multi-valued ACL2 functions
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?.
