algebraic structures on lists

Stream: Is there code for X?

[Hanting Zhang]

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]

what do you do for lists of different lengths?

[Hanting Zhang]

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

[Hanting Zhang]

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