Stream: Is there code for X?
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.
Yakov Pechersky (Mar 17 2021 at 16:37):
what do you do for lists of different lengths?
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
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