Jz Pan

Unfotrunately, I didn't find an easy way to fix this. As you see, the map file actually stores coordinates of each points and the time for the block from a...

I also noticed that. This is because we don't have the font for it 🙁

It's possible but it requires perfect alignment (the player moves in x direction 7 pixels per frame). The following record file `tut09.map-af8e8b89d9df640ec34d90e36475e7af-best-time.mnmsrec` is an example. ~~~ record=0*6,1*12,5,1*12,0*8,1*2,0*15,5,1*14,0*14,5,1*32 seed=9546be9a901716e556d05c35b480544c map(){ name=Fragile...

> I came here to file an issue because I observed the reference to [minpoly.equivAdjoin](https://leanprover-community.github.io/mathlib4_docs/Mathlib/FieldTheory/Minpoly/IsIntegrallyClosed.html#minpoly.equivAdjoin) at [AdjoinRoot.Minpoly.toAdjoin](https://leanprover-community.github.io/mathlib4_docs/Mathlib/RingTheory/AdjoinRoot.html#AdjoinRoot.Minpoly.toAdjoin) doesn't render as a link, only to discover this has already been reported...

> just as it already does not process markdown escape sequences in `code` blocks. This is a natural feature of markdown processor I think. But generally markdown processor (in our...

I think I can try to look at this issue.

> If you teach your filtering about code syntax, then now you have a hacky parser wrapped around a real one, and will almost certainly create more bugs. Unfortunately this...

I am investigating with other solutions. So far I found another markdown parser written in C https://github.com/mity/md4c which claims supporting LaTeX formulas, tables, etc. (Currently we are using https://github.com/commonmark/cmark.) Hopefully...

Maybe there should be a feature which let each module provide a short description of it, and then the doc-gen4 gather all of them to the front page. Not hard-coded...

I think this is related to #43.