damiano
damiano
Just a heads-up that Anne delegated to me #16236 and I will merge is as soon as CI is happy with it. I'm mentioning this since the PR touches the...
@riccardobrasca merging master worked with no changes!
I was under the impression that, as the basic assumptions for the definitions were controversial, this PR may have stayed a PR until someone had a compelling reason to force...
awaiting-review
I view it as follows. `Std` does not impose `lemma` on downstream projects, but offers it with minimal effort. If a user of a downstream project writes `lemma`, they probably...
I think that the argument against `Std` introducing `lemma` is to avoid it straying from the core syntax: there is no interest in introducing `lemma` into core. I am happy...
I personally do not have a preference between the initial version and the new `set_option` switch: I'm happy to go with either. I suspect that most people who will try...
As a test, I ran the linter with the "new" monad on a fresh copy of mathlib: I wanted to make sure that it picked up the same issues that...
Looking at the places where I had to unset the linter, I am guessing that this is just a matter of a slowdown: `notation3`, `theorem`, run_command` all appear among the...
Eric, fair enough! Do you still think that this version is better or should I revert it to the one with the handcrafted `MetaM` state?