How should we redefine the new Finsupp? #12922

Stream: mathlib4

[Miyahara Kō]

How should we redefine the new Finsupp whose structure is aligned to DFinsupp?:

1. Abbreviation

abbrev Finsupp (α : Type*) (M : Type*) [Zero M] :=
  Π₀ _ : α, M

2. Trivial structure of DFinsupp

structure Finsupp (α : Type*) (M : Type*) [Zero M] where ofDFinsupp ::
  toDFinsupp : Π₀ _ : α, M

3. Structure copied from DFinsupp

structure Finsupp (α : Type*) (M : Type*) [Zero M] where mk' ::
  toFun : α → M
  support' : Trunc { s : Multiset α // ∀ a, a ∈ s ∨ toFun a = 0 }

[Miyahara Kō]

/poll How should we redefine the new Finsupp whose structure is aligned to DFinsupp?
Abbreviation
Trivial structure of DFinsupp
Structure copied from DFinsupp

[Eric Wieser]

I'm not convinced that we can reasonably make this change in the order you're implying

[Eric Wieser]

Which is to say; while I'm supportive of your goal here, I think it would be good to write down a more detailed plan of how you plan to get there before bikeshedding too much

[Eric Wieser]

My previous proposal in this direction was to carve out a smaller first step of "rewrite Basis to use DFinsupp", but I also didn't write down how that fits into a larger refactor

[Miyahara Kō]

I've been going using structure copied from DFinsupp, but I'm having trouble with a lot of code duplication and thought I'd solicit opinions on what structure to use.
By the way, this was the plan I had in mind:

1. Change the definition of Finsupp.
2. Finish the rest of the work.

[Miyahara Kō]

Now I will think about it in more detail...

[Miyahara Kō]

I abort this task because it's a hard work and I have no times to do currenlty.
Maybe I restart this task later so I restore this branch.