Theorems · Definition · combinatorics

List.Vector.mOfFn

{m : Type u → Type u_6} → [Monad m] → {α : Type u} → {n : ℕ} → (Fin n → m α) → m (List.Vector α n)

Monadic analog of Vector.ofFn. Given a monadic function on Fin n, return a Vector α n inside the monad.

Defined in

Mathlib.Data.Vector.Basic

Cited by

6 results in Mathlib

Foundations

Depth 26 from the axioms · uses propext

Assumes

Monad