last n elements of a list

Stream: Is there code for X?

[Rob Lewis]

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.

[Mario Carneiro]

list.drop

[Kenny Lau]

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

[Rob Lewis]

That'll do, thanks!

[Kevin Buzzard]

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

[Marc Huisinga]

is the repo private?

[Kevin Buzzard]

Oh rofl it might be :-)

[Kevin Buzzard]

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

[Mario Carneiro]

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

[Mario Carneiro]

(or a PR :smile: )