## Stream: general

### Topic: updating the nth element of a list

#### Scott Morrison (Nov 30 2018 at 01:11):

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 (Nov 30 2018 at 01:12):

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 (Nov 30 2018 at 01:12):

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 (Nov 30 2018 at 01:13):

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 (Nov 30 2018 at 01:13):

Of course there is update_nth

#### Kenny Lau (Nov 30 2018 at 01:14):

also what is it with your meta?

#### Scott Morrison (Nov 30 2018 at 01:14):

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

#### Scott Morrison (Nov 30 2018 at 01:15):

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

#### Scott Morrison (Nov 30 2018 at 01:15):

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 (Nov 30 2018 at 01:16):

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

#### Mario Carneiro (Nov 30 2018 at 03:15):

did you say you want to modify the nth element?

#### Reid Barton (Nov 30 2018 at 03:29):

Did somebody say "lens"?

#### Scott Morrison (Nov 30 2018 at 06:22):

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

#### Keeley Hoek (Dec 01 2018 at 05:29):

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

Last updated: May 14 2021 at 12:18 UTC