Operations using indexes #
@[inline]
def
List.mapFinIdxM
{m : Type u_1 → Type u_2}
{α : Type u_3}
{β : Type u_1}
[Monad m]
(as : List α)
(f : (i : Nat) → α → i < as.length → m β)
:
m (List β)
Given a list as = [a₀, a₁, ...]
and a monadic function f : (i : Nat) → α → (h : i < as.length) → m β
,
returns the list [f 0 a₀ ⋯, f 1 a₁ ⋯, ...]
.
Equations
Instances For
@[specialize #[]]
def
List.mapFinIdxM.go
{m : Type u_1 → Type u_2}
{α : Type u_3}
{β : Type u_1}
[Monad m]
(as : List α)
(f : (i : Nat) → α → i < as.length → m β)
(bs : List α)
(acc : Array β)
:
Auxiliary for mapFinIdxM
:
mapFinIdxM.go [a₀, a₁, ...] acc = acc.toList ++ [f 0 a₀ ⋯, f 1 a₁ ⋯, ...]
Equations
Instances For
@[specialize #[]]
def
List.mapIdxM.go
{m : Type u_1 → Type u_2}
{α : Type u_3}
{β : Type u_1}
[Monad m]
(f : Nat → α → m β)
:
Auxiliary for mapIdxM
:
mapIdxM.go [a₀, a₁, ...] acc = acc.toList ++ [f acc.size a₀, f (acc.size + 1) a₁, ...]
Equations
Instances For
mapFinIdx #
mapIdx #
@[reducible, inline, deprecated List.mapIdx_eq_zipIdx_map (since := "2025-01-21")]
Instances For
@[simp]
@[simp]