feat: add KMP frontend for lists

[fgdorais]

No description provided.

[leanprover-community-bot]

Mathlib CI status (docs):

• ✅ Mathlib branch batteries-pr-testing-1065 has successfully built against this PR. (2024-11-25 09:44:11) View Log
• ✅ Mathlib branch batteries-pr-testing-1065 has successfully built against this PR. (2024-11-25 18:49:22) View Log

[kim-em]

I know this would be revising stuff that already exists, but could we have an API whereby one doesn't ever need to see Matcher, in the common case of just doing a single lookup?

(Perhaps there could be a function directly on List, that takes on optional Matcher argument, with default value that constructs the Matcher?)

[fgdorais]

I'm not sure what these would return. Unlike String there is no Sublist type to work with.

[fgdorais]

I added the same functions as for strings.

[kim-em]

Great, thanks. I'm happy with those.

A naming question, however: List.Sublist already means not-necessarily-contiguous sublist, whereas we use the word "infix" for contiguous sublists. How would you feel about changing the List parts of the API to be consistent with this? (While leaving the String API in terms of Substring, and Array API in terms of Subarray of course.)

[fgdorais]

Names changed.