Stream: PR reviews
Topic: 3709 FTC again
Yury G. Kudryashov (Aug 18 2020 at 19:54):
#3709 is ready for review. I'm writing about this here because it's on the second page.
Johan Commelin (Aug 18 2020 at 20:19):
This is a really cool milestone!
Johan Commelin (Aug 18 2020 at 20:20):
@Patrick Massot @Sebastien Gouezel there's work for you (-;
Yury G. Kudryashov (Aug 18 2020 at 20:50):
The file is long because I repeat many lemmas in slightly different settings (left endpoint, right, both;
(f)deriv(_within) = ...). It would be nice to generate half of the lemmas using some
meta def but I'm not good enough at this.
Patrick Massot (Aug 18 2020 at 21:24):
I think Sébastien is on it (the review work, not metaprogramming).
Last updated: May 06 2021 at 12:15 UTC