Delimiters should go on their own line in multiline docs - Githubissues

leanprover-community / leanprover-community.github.io

Hosts the website for mathlib and other Lean community infrastructure.

https://leanprover-community.github.io/

MIT License

51 stars 119 forks source link

Delimiters should go on their own line in multiline docs #475

Open Rida-Hamadani opened 3 months ago

Rida-Hamadani commented 3 months ago

Check this topic on Zulip.