Zulip Chat Archive
Stream: mathlib4
Topic: Universe variables in mathlib docs have strange spaces
Bhavik Mehta (Sep 04 2023 at 19:47):
image.png
https://leanprover-community.github.io/mathlib4_docs/Mathlib/CategoryTheory/MorphismProperty.html Note in particular maxuv
which the browser thinks is one word, and the four spaces after {v, u}
. This persists for me across browsers
Last updated: Dec 20 2023 at 11:08 UTC