Zulip Chat Archive

Stream: PR reviews

Topic: Irrational Between #8753

Ender Doe (Aug 24 2021 at 16:02):

Bump on #8753. Should be ready for a merge, if reviewers are satisfied with addressed changes.

Scott Morrison (Aug 25 2021 at 00:37):

@Ender Doe, I made some more suggestions. They should be easy. Feel free to ping me here again and I can hit merge when they're done.

Ender Doe (Aug 27 2021 at 22:50):

@Scott Morrison I think the PR should be ready. Based on your and Mario's suggestions, I shrank the theorem to a single existential term mode proof.

Last updated: Dec 20 2023 at 11:08 UTC