Stream: math-comp analysis

Topic: PR status check

view this post on Zulip Zachary Stone (Feb 17 2022 at 23:19):

  1. Regarding !505, it should be good to go? I've completed all the review suggestions. Let me know if you see anything else.
  2. Regarding !527, it should be a reasonably well linted state (linting automation would be great...). If there is something I can do before our next meeting, I'd love to take care of it this weekend. Also, once this stuff is merged, I have the next one ready to go.

As an aside, while working on the Arzela Ascoli stuff, I have found an elegant approach for translating textbook proofs using compact covers into filter language. I suspect the lemma I proved is of more general interest than just for AZ.

view this post on Zulip Reynald Affeldt (Feb 18 2022 at 03:44):

Zachary Stone said:

  1. Regarding !505, it should be good to go? I've completed all the review suggestions. Let me know if you see anything else.

I think it is good to go. I commited a few changes but nothing significant.

view this post on Zulip Reynald Affeldt (Feb 18 2022 at 04:55):

(same for 527)

view this post on Zulip Zachary Stone (Feb 18 2022 at 17:10):

Thank you! I'll merge those shortly.

Last updated: Aug 19 2022 at 21:02 UTC