Theorems about Array.ofFn
#
ofFn #
@[simp]
ofFnM #
def
Array.ofFnM
{m : Type u_1 → Type u_2}
{α : Type u_1}
{n : Nat}
[Monad m]
(f : Fin n → m α)
:
m (Array α)
Construct (in a monadic context) an array by applying a monadic function to each index.
Equations
- Array.ofFnM f = Fin.foldlM n (fun (xs : Array α) (i : Fin n) => xs.push <$> f i) (Array.emptyWithCapacity n)
Instances For
@[simp]
theorem
Array.toList_ofFnM
{m : Type u_1 → Type u_2}
{n : Nat}
{α : Type u_1}
[Monad m]
[LawfulMonad m]
{f : Fin n → m α}
: