English
Definition of a monadic variant of a right fold with index: foldrIdxM takes a monadic function f, a base value b, and a list as, and folds from the right threading monadic effects with index information.
Русский
Определение монадического варианта правой свёртки с индексом: foldrIdxM принимает монадическую функцию f, базовое значение b и список as и свёртывает справа, сохраняя индекс.
LaTeX
$$$\\mathrm{foldrIdxM}(f,b,\\mathrm{as}) = \\mathrm{as}.\\mathrm{foldrIdx}\\bigl(\\lambda i\\, a\\, mb . \\; \\text{обработчик} \\bigr)\\; (\\mathrm{pure}\\, b)$$$
Lean4
/-- Monadic variant of `foldrIdx`. -/
def foldrIdxM {α β} (f : ℕ → α → β → m β) (b : β) (as : List α) : m β :=
as.foldrIdx
(fun i a mb => do
let b ← mb
f i a b)
(pure b)
