MV?

return one or more values 
Major Section:  ACL2-BUILT-INS

Mv? is designed to work with mv?-let, generalizing how mv works with 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 form for any expression, form. 
(let ((y (f x)))
  (declare (type integer y))
  (g x y z))

Logically, (mv? x) is the same as x, while (mv? v1 v2 ...) is the same as (list v1 v2 ...). Also see mv and see mv?-let.