chore: @[expose] List.mapIdxM

src/Init/Data/List/MapIdx.lean

@@ -61,7 +61,7 @@ proof that the index is valid.
 `List.mapIdxM` is a variant that does not provide the function with evidence that the index is
 valid.
 -/
-@[inline] def mapFinIdxM [Monad m] (as : List α) (f : (i : Nat) → α → (h : i < as.length) → m β) : m (List β) :=
+@[inline, expose] def mapFinIdxM [Monad m] (as : List α) (f : (i : Nat) → α → (h : i < as.length) → m β) : m (List β) :=
   go as #[] (by simp)
 where
   /-- Auxiliary for `mapFinIdxM`:
@@ -78,7 +78,7 @@ found, returning the list of results.
 `List.mapFinIdxM` is a variant that additionally provides the function with a proof that the index
 is valid.
 -/
-@[inline] def mapIdxM [Monad m] (f : Nat → α → m β) (as : List α) : m (List β) := go as #[] where
+@[inline, expose] def mapIdxM [Monad m] (f : Nat → α → m β) (as : List α) : m (List β) := go as #[] where
   /-- Auxiliary for `mapIdxM`:
   `mapIdxM.go [a₀, a₁, ...] acc = acc.toList ++ [f acc.size a₀, f (acc.size + 1) a₁, ...]` -/
   @[specialize] go : List α → Array β → m (List β)