def
List.ofFnM
{m : Type u_1 → Type u_2}
{α : Type u_1}
{n : Nat}
[Monad m]
(f : Fin n → m α)
:
m (List α)
Creates a list wrapped in a monad by applying the monadic function f : Fin n → m α
to each potential index in order, starting at 0
.
Equations
- List.ofFnM f = List.reverse <$> Fin.foldlM n (fun (xs : List α) (i : Fin n) => (fun (x : α) => x :: xs) <$> f i) []
Instances For
See Init.Data.List.FinRange
for the ofFnM_succ
variant.