List.removeNth vs List.eraseIdx

Stream: batteries

[Yury G. Kudryashov]

It looks like docs#List.removeNth from Std is the same as docs#List.eraseIdx from core.

[Yury G. Kudryashov]

@Mario Carneiro What do you prefer to do? Drop Std version (probably, making it a deprecated alias first)? Something else?

[Yury G. Kudryashov]

@Mario Carneiro Ping here.

[Yury G. Kudryashov]

#12388 adds lemmas about eraseIdx to Mathlib. Should I leave it as is, or migrate to removeNth?

[Yury G. Kudryashov]

#xy: I want to redefine docs#Finset.offDiag based on

def offDiag (l : List α) : List (α × α) :=
  l.enum.bind fun nx ↦ map (Prod.mk nx.2) <| l.eraseIdx nx.1

[Mario Carneiro]

Drop the std version makes sense

[Yury G. Kudryashov]

OK, I'll prepare a PR over the weekend.

[Yury G. Kudryashov]

std4#781 #12660