English
Auxiliary definition for a monadic map with index: mapIdxMAux' takes a function f and returns a function that processes a list with an index, threading monadic effects.
Русский
Вспомогательное определение для монадического отображения с индексом: mapIdxMAux' принимает функцию и возвращает функцию, обрабатывающую список с учётом индекса, сохраняя монадические эффекты.
LaTeX
$$$\\mathrm{mapIdxMAux'}(f)(i,[]) = \\mathrm{pure}\\langle\\rangle \\\\ \\\\ \\mathrm{mapIdxMAux'}(f)(i,a:as) = f(i,a) *> \\mathrm{mapIdxMAux'}(f)(i+1,as)$$$
Lean4
/-- Auxiliary definition for `mapIdxM'`. -/
def mapIdxMAux' {α} (f : ℕ → α → m PUnit) : ℕ → List α → m PUnit
| _, [] => pure ⟨⟩
| i, a :: as => f i a *> mapIdxMAux' f (i + 1) as
