Gabriel Ebner

Hiding the scrollbars (for the left and right navigation sidebar) was an intentional decision. I found it confusing to have 2 scrollbars on the right visible at all times. Zulip...

What is the story for the *.lean files here? Are these installed as well? > Since bors isn't enabled in this repository, if we do decide to merge this we...

> No, not yet - but the python code doesn't use these at all yet. Hmm, but is there anything you can do with the python code alone? Related question:...

#deploy

#deploy

The reason for the `.bmp` extension instead of `.json` is that github will then *automatically* gzip it. See https://github.com/leanprover-community/doc-gen/pull/125

#deploy

Any idea what went wrong? #deploy

Yeah, I can add it in firefox but not in chromium. And searching with spaces is not supported: https://leanprover-community.github.io/mathlib_docs_demo/find/nat+cast

A related problem is that the documentation itself should print the exported name instead of `decidable.to_bool`: