English
Apply a monadic function to each component of a vector, returning a vector inside the same monad.
Русский
Применить монадическую функцию к каждому компоненту вектора, получить вектор в той же монадe.
LaTeX
$$$\\mathrm{mmap} : [\\mathrm{Monad}\\ m] \\Rightarrow {\\;}{\\alpha} \\to {\\beta} \\, (\\mathrm{Vector}\\ \\alpha\\ n) \\to m(\\mathrm{Vector}\\ \\beta\\ n)$$$
Lean4
/-- Apply a monadic function to each component of a vector,
returning a vector inside the monad. -/
def mmap {m} [Monad m] {α} {β : Type u} (f : α → m β) : ∀ {n}, Vector α n → m (Vector β n)
| 0, _ => pure nil
| _ + 1, xs => do
let h' ← f xs.head
let t' ← mmap f xs.tail
pure (h' ::ᵥ t')
