MV?-LET

calling possibly multi-valued ACL2 functions
Major Section:  PROGRAMMING

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