Zulip Chat Archive

Stream: Is there code for X?

Topic: last n elements of a list


view this post on Zulip Rob Lewis (Apr 21 2020 at 08:36):

I'm very surprised I can't find this -- is there a function ℕ → list _ → list _ that gets the last n elements of the list? I don't care about the behavior when n is too big.

view this post on Zulip Mario Carneiro (Apr 21 2020 at 08:37):

list.drop

view this post on Zulip Kenny Lau (Apr 21 2020 at 08:38):

list.drop (list.length L - n) L

view this post on Zulip Rob Lewis (Apr 21 2020 at 08:40):

That'll do, thanks!

view this post on Zulip Kevin Buzzard (Apr 21 2020 at 09:17):

My student Ellen Arlt needed a bunch of things about lists which she couldn't find in data.list.basic. Some of what she needed is here: https://github.com/ImperialCollegeLondon/dots_and_boxes/blob/master/src/sle/lemmas.lean . My impression was that there are some easy holes to be filled here, especially with regards to nth_le

view this post on Zulip Marc Huisinga (Apr 21 2020 at 09:23):

is the repo private?

view this post on Zulip Kevin Buzzard (Apr 21 2020 at 09:34):

Oh rofl it might be :-)

view this post on Zulip Kevin Buzzard (Apr 21 2020 at 09:34):

It's about 20 lemmas which should be in data.list.basic

view this post on Zulip Mario Carneiro (Apr 21 2020 at 09:34):

you could put them in a gist if you don't want to make the repo public

view this post on Zulip Mario Carneiro (Apr 21 2020 at 09:35):

(or a PR :smile: )


Last updated: May 17 2021 at 16:26 UTC