list.nth_le

Stream: mathlib4

[Yury G. Kudryashov]

I see that docs#list.nth and docs#list.nthd are called docs4#List.get? and docs4#List.getD in Lean 4. What shoudl we do about docs#list.inth and docs#list.nth_le? For the former, we can't use docs4#List.get! because it panics on the empty list. For the latter, docs#List.nth is very similar but it bundles arguments into a Fin l.length, so lemmas like docs#list.nth_le_tail will look weird. What should we do?

[Mario Carneiro]

We should try to align list.nth_le to List.get where possible, I think

[Mario Carneiro]

we can have an unbundled version if necessary, say List.get'

[Mario Carneiro]

list.inth should become List.getI

[Mario Carneiro]

note that most theorems about lists are automatically on the short list to move to Std, but it's fine to PR them to mathlib4 first

[Yury G. Kudryashov]

What should we do with lemmas like docs#list.nth_le_tail?

[Yury G. Kudryashov]

How would you formulate it with def list.get (l : list α) (n : fin l.length) : α := l.nth_le n n.is_lt?