glossary

Stream: Zulip meta

[Johan Commelin]

Can/should we have a linkifier for glossary#diamond ?

[Kevin Buzzard]

More generally should we have linkifiers for everything mentioned in https://leanprover-community.github.io/glossary.html#diamond ?

[Kevin Buzzard]

(or perhaps, more reasonably, for many such things)

[Shing Tak Lam]

I think Johan is suggesting glossary#foo goes to the entry about foo in the glossary? Although some of the ids that are generated for the titles aren't great for that purpose, eg. (heavy-coderflcode--heavy-codereflcode)

[Julian Berman]

Right I saw that

[Julian Berman]

I'm gonna fix that in a PR later

[Julian Berman]

(by at least removing all the backticks from the titles)

[Julian Berman]

OK, thanks to Bryan, this was merged, so though it's a bit harder to discover these (you need to open Developer Tools or otherwise look at the HTML), you can now write #heavy-rfl for that one, or glossary#heavy-rfl as soon as we have that linkifier.

[Bryan Gin-ge Chen]

glossary#heavy-rfl

[Bryan Gin-ge Chen]

Looks like it works!

Regarding discoverability, I think if we could get the # which pop up when you hover over the heading to give the nicer anchor, that'd probably be sufficient.

[Bryan Gin-ge Chen]

(That'll require messing with the python code though.)

[Gabriel DORIATH DÖHLER]

Should HoTT, UH (unification hints), TC (type classes) and fbip (functional but in place) be added to the glossary ? As a newcomer I would find it useful as acronyms are hard to search for.

[Anne Baanen]

Sounds like a good idea! I think we should also include "dot notation" (a.k.a. "field notation" or "generalized (structure) projections" in the Lean 3 source code)

[Stuart Presnell]

Maybe also “API”?

[Julian Berman]

All the above definitely seem like good ideas to me too -- maybe put them in an issue ticket so they're tracked -- I haven't made any glossary progress in a week or two, but will get back to it soon unless someone else beats me to these.

[Gabriel DORIATH DÖHLER]

https://github.com/leanprover-community/leanprover-community.github.io/issues/226

[Anne Baanen]

Created a PR for explaining dot notation

[Eric Taucher]

Anne Baanen said:

Created a PR for explaining dot notation

When I first read that I thought of GraphViz dot notation, then realized it probably means list without the syntactic sugar, e.g.

[a,b,c] is

.(a,.(b,.(c,[])))

[Patrick Massot]

It's neither of these explanations. Let's put it in the glossary...