TheoremDoc: Usage of [[mathlib_doc]] not documented

[JadAbouHawili]

I was able to discover [[mathlib_doc]] by playing around in my ide and hovering over stuff, but [[mathlib_doc]] is not discussed in the documentation. Any mention of [[mathlib_doc]] is tucked away in server/GameServer/Commands.lean. Shouldn't doc/ discuss it because its hard to notice [[mathlib_doc]] if it isn't mentioned in doc/

[joneugster]

Oh I thought that was a feature that was never completed/working, but it's certainly on my schedule to do that

[JadAbouHawili]

well, for some things it generated the right link but for others it didn't.(but it might be me using it wrong, because it says you need to have the name match whats in mathlib, which is a bit vague)
In any case, I think it should get a mention in doc/ regardless, maybe even stating that its a work in progress. Someone might see this and decide to contribute.