updating the nth element of a list

Stream: general

[Scott Morrison]

Do we have something equivalent to

def patch_nth {α : Type} (f : α → α) : ℕ → list α → list α
| _ []           := []
| 0 (h :: t)     := f h :: t
| (n+1) (h :: t) := h :: patch_nth n t

in mathlib?

[Scott Morrison]

I've found a few times that it's really painful for update the nth element, because you have to deal with nth returning an option, even when you know it's there.

[Scott Morrison]

A slight variation that is even more useful:

def opatch_nth {α : Type} (f : α → option α) : ℕ → list α → list α
| _ []           := []
| 0 (h :: t)     := match f h with
                    | (some e) := e :: t
                    | none     := t
                    end
| (n+1) (h :: t) := h :: opatch_nth n t

[Kenny Lau]

I've found a few times that it's really painful for update the nth element, because you have to deal with nth returning an option, even when you know it's there.

... did you say it's painful to update the nth element?

[Scott Morrison]

Of course there is update_nth

[Kenny Lau]

also what is it with your meta?

[Scott Morrison]

Oh, yeah, those metas are completely unnecessary :-) Just habit, as I was in a whole file where most things were meta.

[Scott Morrison]

But to use update_nth, you need to use nth earlier to get out the existing element to modify.

[Scott Morrison]

The typical example here is that I have a list of some structure, and I want to modify a single field of the nth element.

[Scott Morrison]

In this case the function f can be λ s, { f := x, .. s}.

[Mario Carneiro]

did you say you want to modify the nth element?

[Reid Barton]

Did somebody say "lens"?

[Scott Morrison]

Thanks. And yes, let's have more lens. :-)

[Keeley Hoek]

Wait, isn't the syntax to declare functions in lean meta def ....? ;)