English
Monadic analogue of building a vector from a function on Fin n: given f: Fin n → m α, return m (Vector α n) by taking the first element from f(0) and recursing on the tail.
Русский
Монадический аналог построения вектора из функции на Fin n: дано f: Fin n → m α, вернуть m (Vector α n) беря первый элемент из f(0) и рекурсивно обрабатывая хвост.
LaTeX
$$$\\mathrm{mOfFn} : \\forall {m} [\\mathrm{Monad}\\ m] {\\alpha} {n}, (\\mathrm{Fin}\\ n \\to m\\alpha) \\to m(\\mathrm{Vector}\\ \\alpha\\ n)$$$
Lean4
/-- Monadic analog of `Vector.ofFn`.
Given a monadic function on `Fin n`, return a `Vector α n` inside the monad. -/
def mOfFn {m} [Monad m] {α : Type u} : ∀ {n}, (Fin n → m α) → m (Vector α n)
| 0, _ => pure nil
| _ + 1, f => do
let a ← f 0
let v ← mOfFn fun i => f i.succ
pure (a ::ᵥ v)
