Theorems about Vector.ofFn
#
ofFnM #
def
Vector.ofFnM
{m : Type u_1 → Type u_2}
{α : Type u_1}
{n : Nat}
[Monad m]
(f : Fin n → m α)
:
m (Vector α n)
Construct (in a monadic context) a vector by applying a monadic function to each index.
Equations
- Vector.ofFnM f = Vector.ofFnM.go f 0 ⋯ (Array.emptyWithCapacity n) ⋯
Instances For
@[simp]
theorem
Vector.toArray_ofFnM
{m : Type u_1 → Type u_2}
{n : Nat}
{α : Type u_1}
[Monad m]
[LawfulMonad m]
{f : Fin n → m α}
:
@[simp]
theorem
Vector.toList_ofFnM
{m : Type u_1 → Type u_2}
{n : Nat}
{α : Type u_1}
[Monad m]
[LawfulMonad m]
{f : Fin n → m α}
: