Commit 2023-09-10 13:28 a5c70379

feat(Data/Finsupp): add notation (#6367) This PR provides fun₀ | 3 => a | 7 => b notation for Finsupp, which desugars to Finsupp.update and Finsupp.single, in the same way that {a, b} desugars to insert and singleton. It also provides a matching delaborator: as an example of the effect of this, Finsupp.single_add now shows as:

Finsupp.single_add.{u_2, u_1} {α : Type u_1} {M : Type u_2} [inst✝ : AddZeroClass M] (a : α) (b₁ b₂ : M) :
  (fun₀ | a => b₁ + b₂) = (fun₀ | a => b₁) + fun₀ | a => b₂

Finally, it provides a Repr instance; though this is somewhat misleading as the syntax that is produced by Repr isn't actually computable so can't round-trip! Discussed on Zulip here.