idiomatic Lean for python L[a:b]

Stream: general

[Kevin Buzzard]

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]

list.remove_nth?

[Kevin Buzzard]

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

[Kevin Buzzard]

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

[Rob Lewis]

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

[Kevin Buzzard]

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.