Zulip Chat Archive

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; 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.

Patrick Massot (Aug 18 2020 at 21:24):

I think Sébastien is on it (the review work, not metaprogramming).

Last updated: Dec 20 2023 at 11:08 UTC