Zulip Chat Archive

Stream: general

Topic: updating the nth element of a list


view this post on Zulip 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?

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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?

view this post on Zulip Scott Morrison (Nov 30 2018 at 01:13):

Of course there is update_nth

view this post on Zulip Kenny Lau (Nov 30 2018 at 01:14):

also what is it with your meta?

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Scott Morrison (Nov 30 2018 at 01:16):

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

view this post on Zulip Mario Carneiro (Nov 30 2018 at 03:15):

did you say you want to modify the nth element?

view this post on Zulip Reid Barton (Nov 30 2018 at 03:29):

Did somebody say "lens"?

view this post on Zulip Scott Morrison (Nov 30 2018 at 06:22):

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

view this post on Zulip 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