Why isn't `Fin` used in the definitions of `mapFinIdx`?

Stream: new members

[Scott Buckley]

I've noticed that mapFinIdx in List is defined as follows (and similarly in Array):

def mapFinIdx (as : List α) (f : (i : Nat) → α → (h : i < as.length) → β) : List β

Is there any reason it isn't instead defined as follows:

def mapFinIdx (as : List α) (f : (i : Fin as.length) → α → β) : List β

I was just writing some of my own helpers for something which I ended up replacing with uses of mapFinIdx, but it seems strange to me that the index and its in-range proof are carried around separately, rather than packaged inside Fin, especially given the name of the method contains "Fin".

I'm not trying to start an argument, just trying to get some insight into that design decision. I searched Zulip history with no luck, but if there's another way I should look for this kind of info please let me know. Thank you!

[Vlad Tsyrklevich]

Looking at the git blame I found lean4#6697 but I'm not entirely sure what the 'rest of the API' means here. It better matches mapIdx for example, but not sure if the motivation was broader than that.

[Vlad Tsyrklevich]

(I'd also be curious to know if there's a reason the hypothesis is after \a, it seems more natural to have it closer to the index.)

[Jakub Nowak]

From my experience unbundled is easier to work with. Compared to bundled you don't have to deal with coercion and simp cannot unbundle the proof. But tbh, I'd rather we fix the problems with using bundled version instead of changing to unbundled.