Repr for Finsupp

Stream: mathlib4

[Snir Broshi]

I noticed that it is possible to print a Finset but not a Finsupp, which is a function with finite support.
I suggest the following:

import Mathlib
variable {α M : Type*}
variable [Zero M]

unsafe instance [Repr α] [Repr M] : Repr (Finsupp α M) where
  reprPrec f _ := Std.Format.paren (Std.Format.joinSep
    (f.support.val.unquot.map (fun x => repr x ++ " ↦ " ++ repr (f x)) ++ ["_ ↦ " ++ repr (0 : M)])
    (";" ++ Std.Format.line)
  )

As an example, here's how the prime factorization of a number looks like:

#eval Nat.factorization 5040
-- (2 ↦ 4; 3 ↦ 2; 5 ↦ 1; 7 ↦ 1; _ ↦ 0)

The syntax is roughly based on notation from Rocq's Software Foundations.

I'm not sure which brackets (( or [ or {) and separator (; or ,) are the best for this.
What do you think?

Also, should there be a corresponding notation for constructing Finsupp?

[Aaron Liu]

Could we make this notation parsable back into a Finsupp?

[Ruben Van de Velde]

I thought we had one, like fin_0 or something

[Snir Broshi]

I'm not sure how to implement notation like this, do you know where the Set notation is implemented for reference?
I found docs#Insert which is somehow related to the notation

[Snir Broshi]

This is the current syntax:
fun n ↦ match n with | 2 => 4 | 3 => 2 | 5 => 1 | 7 => 1 | _ => 0
although it doesn't know that it's a Finsupp ℕ ℕ.
Should we use | for separators in the Repr?

[Eric Wieser]

I think we already have a repr for Finsupp?

[Eric Wieser]

docs#Finsupp.instRepr

[Snir Broshi]

Oh, I tried #synth Repr (Finsupp α M) and got nothing, because I didn't import Mathlib.Data.Finsupp.Notation :sweat:
Sorry

[Eric Wieser]

Generally it's better to import mathlib when trying to find out if something exists