## Stream: general

### Topic: idiomatic Lean for python L[a:b]

#### Kevin Buzzard (Nov 19 2019 at 15:39):

I want to do things like remove the n'th element of a list (decreasing its size by 1) and similar. Do we have this in Lean? I guess in Python I'd do something like L[:n]++L[n+1:]

#### Rob Lewis (Nov 19 2019 at 15:40):

list.remove_nth?

#### Kevin Buzzard (Nov 19 2019 at 15:42):

Oh excellent. I've been staring at data.list.basic but it's so big!

#### Kevin Buzzard (Nov 19 2019 at 15:43):

oh man the definition is in core :-/ I should have known, with lists. Thanks Rob!

#### Rob Lewis (Nov 19 2019 at 15:45):

I just guessed the name because you wanted to remove the n 'th element.

#### Kevin Buzzard (Nov 19 2019 at 15:49):

I don't think I've ever removed anything in Lean before. I'm a bit surprised it's not called rm or something, but there you go. This is great, thanks.

Last updated: May 13 2021 at 06:15 UTC