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
Rob Lewis (Nov 19 2019 at 15:40):
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
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