leanprover
multi-lang support
It would be nice if there was a function to support translation into other languages.
The mdbook currently used for documentation does not support this.
Can you say a bit more about what your needs would be here?
I don't plan to build support for translations in the next year, but if there's some minimal hook I can provide the API that lets others do it, then great! I do plan to support non-English languages in the relatively near future, however, so a Danish-language text might say "kapitel" and "indholdsfortegnelse" instead of "chapter" and "table of contents".
It is not about translating the verso UI, it is about the ability to support translating documents made by verso. it's i18n for verso.
I think there is a demand for translating documents such as functional programming in lean, for example, into languages other than English.