Document use of Unicode symbols on a per-module basis

[jamesmckinna]

Lifted out from #2595 : rather than document symbol usage in style-guide, document there only the guideline that each module which introduces new (infix) Unicode symbols should document their encodings in the module where they are introduced. Cf. the didactic style adopted in PLFA

For discussion:

• location: in opening comment, or in a 'symbol table' at the end of the module?
• how much to we deal with the existing legacy symbology?
• ...

[JacquesCarette]

I definitely prefer documentation to be at top. Things at the end are a kind of 'oh, by the way' -- which works for PLFA, but not so much for stdlib, IMHO.

Legacy: I'd say we do incremental improvements as we have time to (or have new students who need learning tasks to get going).

[MatthewDaggitt]

I'd prefer them to be attached to the definition of the symbol itself rather than at a table at the top?

[jamesmckinna]

Thanks for the swift and constructive feedback!
I think it is worth considering these things as attributes akin to fixity, so I like @MatthewDaggitt 's suggestion of them being really in place.

That said, such a choice seems to leave us with only M-. navigation in emacs Agda mode to find such things (so no worse than the status quo), but the idea of a table was about collecting them together ... and like any redundant recoding, a potential source of knock-on viscosity... like all non-checked documentation. It feels as though there's a tougher problem to crack there, lurking off-stage...

[jwaldmann]

now it's a bit late for April Fool's, but ... have you considered using emojis in stdlib to further decrease read-, pronounce-, and writeability?

[jamesmckinna]

@jwaldmann I'm not clear about the intention behind your message, but if you have specific problems with the issue, or more generally with how the library developers/maintainers contribute positively or negatively to stdlib, then by all means raise specific issues (such as: 'avoid Unicode in favour of prefix ASCII names', for example).

If instead there is a problem with the way any particular person expresses themselves here, the perhaps that's something better done in private correspondence?

[jwaldmann]

sure. it was an attempt at a joke (about the appearance of stdlib, not anything personal). I have full respect for the work that goes into this project. I am sorry if the joke created to opposite impression.

[gallais]

like all non-checked documentation

If we're going to do that then that documentation should 100% be generated by the CI
using a simple Haskell program collecting such symbols and patching the docs emitted
by Agda's html backend.

When you're looking at source code your editor should already be able to tell you
information about the character you're looking at.