User-friendly notation command

[hrmacbeth]

Currently, subtle notations like ∑ and ⋃ all need their own delaborators. Since it takes more expertise to write the delaborator than to set up the notation, we have many ported files "implementing" notation which never displays in the infoview.

To quote from a Zulip thread where this was discussed,

At a high level, the point is that Lean 3's notation table was intrinsically invertible (at least in theory). Being able to define elaborators and delaborators separately is much more powerful, but you do lose that automatic invertibility.

Would it be worth writing a special command for invertible notation, which works in a smaller set of cases but is more user-friendly (replicating the lean 3 experience) in those cases?

Yeah ... figure out what would be a good notation command that would make things at least as user-friendly as the Lean 3 one (including invertibility).

notation3 is exactly what you need to get an unexpander automatically since the allowed syntax there is rigid enough that we know what to generate. I think it would not be too difficult to adapt Kyle's unexpander to work on arbitrary notation3s

[kmill]

4533 is for notation3 pretty printing.

I think it could eventually handle ∑'s in notation fairly easily too.