Floris van Doorn
Floris van Doorn
bors merge bors d+ I think the deprecations make it fine to not list the renames.
I don't think it's feasible to generalize universe metavariables in definitions before elaborating the value. As mentioned in #4482, that will lead to huge inconveniences. I don't think that the...
Ok, this happens only rarely in Mathlib, so I think the fallout will be limited. After that I think the only issue is in definitions.
probably causing the bors failure After the batch is merged, please merge master bors r- bors d+
That is fair. I don't actually feel strongly about seeing the declaration. However, I think the following three things are important: * Occurrences of `CommMonoid.toMonoid` in the doc should be...
This looks very nice from a readability standpoint. Also, the reactions on Zulip are overwhelmingly positive. Am I correct that the current status of the delaboration is only that `in`...
Ah, thanks for the link. I think we should merge this. The notation is a lot nicer, and it shouldn't be too bad for users to adapt to this. bors...
Nope, it can be any word or a single letter, highlighted or not. I expect that it has to do with the fact that some markup is copied with it....
bors merge