Data.List.Indexes !4#1812

Stream: mathlib4

[Johan Commelin]

This file has some troubles because a definition changed. So it ports the Lean 3 version as

protected def oldMapIdxCore (f : ℕ → α → β) : ℕ → List α → List β
  | _, []      => []
  | k, a :: as => f k a :: List.oldMapIdxCore f (k + 1) as

and later proves equality with mapIdxCore etc...

I think the approach is fine during the port. Should we use the old prefix for such occasions? Or rather a ' suffix?

[Eric Wieser]

docs4#List.mapIdx, docs#list.map_with_idx

[Johan Commelin]

I kicked this on the queue