Zulip Chat Archive

Stream: PR reviews

Topic: 3709 FTC again


view this post on Zulip 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.

view this post on Zulip Johan Commelin (Aug 18 2020 at 20:19):

This is a really cool milestone!

view this post on Zulip Johan Commelin (Aug 18 2020 at 20:20):

@Patrick Massot @Sebastien Gouezel there's work for you (-;

view this post on Zulip 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; has_strict_(f)deriv_at, has_(f)deriv_at, has_(f)deriv_within_at, (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.

view this post on Zulip 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