Zulip Chat Archive

Stream: mathlib4

Topic: list.nth_le


Yury G. Kudryashov (Nov 25 2022 at 06:28):

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 (Nov 25 2022 at 07:33):

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

Mario Carneiro (Nov 25 2022 at 07:34):

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

Mario Carneiro (Nov 25 2022 at 07:34):

list.inth should become List.getI

Mario Carneiro (Nov 25 2022 at 07:36):

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 (Nov 25 2022 at 08:21):

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

Yury G. Kudryashov (Nov 25 2022 at 08:21):

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


Last updated: Dec 20 2023 at 11:08 UTC