grunweg
grunweg
Another idea for scope creep: - do you think it's useful to say that *named instances* need not be deprecated? (That question also came up occasionally.)
There was also https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/Deprecation.20policy, trying to gather consensus on a mathlib policy. I never followed through on documenting that... and some aspects are outdated now (for the better). The thread...
Thanks; I like your new version. There might always be ways to word-smith, but what's here looks good enough to me. I'll cross-post on zulip to get some more eyes...
I just came here from [zulip](https://leanprover.zulipchat.com/#narrow/channel/270676-lean4/topic/Loogle.20feature.20request.3A.20hide.20deprecated.20aliasses/with/501197015): I would be very happy to see deprecated aliasses omitted. I don't have an equally opinion about deprecated definitions; "whatever is more convenient to...
Sure, I agree. Can you add the default target bit to the PR description? (I cannot.)
FYI: #15278, #15279, #15280 (edit: and #15283) fix some easy linter errors; I don't have further fixes in the pipeline
Do you know how to do this? (You can also leave a pointer here and I'll try to add this to the linter, when I find time. This week, and...
!bench
(I worry if the linter implementation is too slow right now, and the linters should rather be merged... let's benchmark to find out!)
!bench