Zulip Chat Archive

Stream: general

Topic: Splitting up algebra.pointwise

Yaël Dillies (Mar 15 2022 at 01:18):

Are people in favor of splitting up file#algebra/pointwise? #12694 adds 140 lines (for a total of 1.5k) and my next PR will add ~600 lines of finset operations.

The one way I see we could split it up is into

  • algebra.pointwise.finset
  • algebra.pointwise.set

Feel free to come up with better!

Bhavik Mehta (Mar 15 2022 at 01:20):

I'm in favour of this

Eric Wieser (Mar 15 2022 at 01:27):

I think a lot of the existing imports will only need the set version, so that seems like a good split to me

Floris van Doorn (Mar 15 2022 at 08:01):

Since we also have order.filter.pointwise (and various others), how about doing the same split, but moving them to data.set.pointwise and data.finset.pointwise?

Yaël Dillies (Mar 15 2022 at 09:37):

Yeah why not!

Yaël Dillies (Mar 19 2022 at 18:16):

While we're at it, I just noticed file#algebra/algebra/operations. Shouldn't it be called algebra.algebra.pointwise?

Yaël Dillies (Mar 19 2022 at 21:05):


Last updated: Dec 20 2023 at 11:08 UTC