TheoremDoc: Usage of [[mathlib_doc]] not documented
JadAbouHawili opened this issue · 2 comments
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/
Oh I thought that was a feature that was never completed/working, but it's certainly on my schedule to do that
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.