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