Theorems about Vector.ofFn
#
ofFnM #
@[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 α}
: