Zulip Chat Archive
Stream: general
Topic: see Note [default priority]
Kevin Buzzard (Dec 19 2019 at 19:51):
Where can I see this note? It's appearing everywhere in mathlib nowadays
Johan Commelin (Dec 19 2019 at 20:03):
Can't grep help you out?
Johan Commelin (Dec 19 2019 at 20:03):
Some time soon you will be able to see this in the generated docs as well. The docs are very rapidly evolving this week.
Rob Lewis (Dec 19 2019 at 20:09):
Some time soon
- as of this morning. https://leanprover-community.github.io/mathlib_docs/notes.html
Kevin Buzzard (Dec 19 2019 at 20:10):
Another question I had regarding recent changes: what is an abbreviation?
Kevin Buzzard (Dec 19 2019 at 20:11):
Oh this is in TPIL!
Last updated: Dec 20 2023 at 11:08 UTC