Zulip Chat Archive

Stream: Is there code for X?

Topic: algebraic structures on lists


view this post on Zulip Hanting Zhang (Mar 17 2021 at 16:35):

Is there anything for index-wise addition on lists? Or a monoid structure? I couldn't find anything in mathlib and I wonder if it's because no one has done them yet, or because they were intentionally omitted.

view this post on Zulip Yakov Pechersky (Mar 17 2021 at 16:37):

what do you do for lists of different lengths?

view this post on Zulip Hanting Zhang (Mar 17 2021 at 16:44):

I'm not sure. I guess I would truncate to the smaller length, which would agree with list.map\2.

view this post on Zulip Hanting Zhang (Mar 17 2021 at 16:46):

Ohh. It's in docs#list.func.add. :upside_down:


Last updated: May 16 2021 at 05:21 UTC