List.nextOr

Stream: mathlib4

[Yury G. Kudryashov]

Currently, we have docs#List.nextOr which should be named List.nextD according to the current naming convention. We also have List.next and List.prev but no List.prevOr/prevD.

[Yury G. Kudryashov]

Before migrating from get to getElem, I'm trying to cleanup API a bit (e.g., some lemmas assume both a ∈ l and a ∈ x::l).

[Yury G. Kudryashov]

What should I do:

• drop nextOr?
• rename it to nextD?
• add next? instead?

[Yakov Pechersky]

How would you define next without nextOr?

[Yury G. Kudryashov]

You're right, the only options are nextD and next?