Lemmas about List.*Idx functions.

Some specification lemmas for List.mapIdx, List.mapIdxM, List.foldlIdx and List.foldrIdx.

As of 2025-01-29, these are not used anywhere in Mathlib. Moreover, with List.enum and List.enumFrom being replaced by List.zipIdx in Lean's nightly-2025-01-29 release, they now use deprecated functions and theorems. Rather than updating this unused material, we are deprecating it. Anyone wanting to restore this material is welcome to do so, but will need to update uses of List.enum and List.enumFrom to use List.zipIdx instead. However, note that this material will later be implemented in the Lean standard library.

theorem List.mapIdx_append_one {α : Type u} {β : Type v} {f : ℕ → α → β} {l : List α} {e : α} : mapIdx f (l ++ [e]) = mapIdx f l ++ [f l.length e]

theorem List.mapIdx_eq_ofFn {α : Type u} {β : Type v} (l : List α) (f : ℕ → α → β) : mapIdx f l = ofFn fun (i : Fin l.length) => f (↑i) (l.get i)

theorem List.mapIdxMAux'_eq_mapIdxMGo {m : Type u → Type v} [Monad m] [LawfulMonad m] {α : Type u_1} (f : ℕ → α → m PUnit) (as : List α) (arr : Array PUnit) : mapIdxMAux' f arr.size as = mapIdxM.go f as arr *> pure PUnit.unit

theorem List.mapIdxM'_eq_mapIdxM {m : Type u → Type v} [Monad m] [LawfulMonad m] {α : Type u_1} (f : ℕ → α → m PUnit) (as : List α) : mapIdxM' f as = mapIdxM f as *> pure PUnit.unit