Major Section: ACL2-BUILT-INS
Mv? is designed to work with
mv?-let, generalizing how
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
formfor any expression,
(let ((y (f x))) (declare (type integer y)) (g x y z))
(mv? x) is the same as
(mv? v1 v2 ...) is the
(list v1 v2 ...). Also see mv and see mv?-let.