Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

[Merged by Bors] - chore: scope open Classical #11199

Closed
wants to merge 16 commits into from
Closed

[Merged by Bors] - chore: scope open Classical #11199

wants to merge 16 commits into from

Commits on Mar 6, 2024

  1. deal with open Classical( in)?$

    @ericrbg
    ericrbg committed Mar 6, 2024
    Configuration menu
    Copy the full SHA
    35ad9d9 View commit details
    Browse the repository at this point in the history

  2. some edge cases that were messing up our next regex

    @ericrbg
    ericrbg committed Mar 6, 2024
    Configuration menu
    Copy the full SHA
    5979cb8 View commit details
    Browse the repository at this point in the history

  3. deal with open Classical(.+) 

    replace with `open scoped Classical\nopen $1`
    @ericrbg
    ericrbg committed Mar 6, 2024
    Configuration menu
    Copy the full SHA
    80b35b7 View commit details
    Browse the repository at this point in the history

  4. deal with open ([^s].*) Classical( ?)(.*) 

    we replace with `open scoped Classical\nopen $1$2$3`
    @ericrbg
    ericrbg committed Mar 6, 2024
    Configuration menu
    Copy the full SHA
    3c354ee View commit details
    Browse the repository at this point in the history

  5. fix nontrivial/basic

    @ericrbg
    ericrbg committed Mar 6, 2024
    Configuration menu
    Copy the full SHA
    b8e0052 View commit details
    Browse the repository at this point in the history

  6. fix Order/Chain; use Exists.choose

    @ericrbg
    ericrbg committed Mar 6, 2024
    Configuration menu
    Copy the full SHA
    c337683 View commit details
    Browse the repository at this point in the history

  7. fix a hiding oops

    @ericrbg
    ericrbg committed Mar 6, 2024
    Configuration menu
    Copy the full SHA
    39b8ae9 View commit details
    Browse the repository at this point in the history

  8. fix settheory/cardinal/basic

    @ericrbg
    ericrbg committed Mar 6, 2024
    Configuration menu
    Copy the full SHA
    0f67c24 View commit details
    Browse the repository at this point in the history

  9. LiminfLimsup -> Exists.choose

    @ericrbg
    ericrbg committed Mar 6, 2024
    Configuration menu
    Copy the full SHA
    e3609d4 View commit details
    Browse the repository at this point in the history

  10. fix tsum

    @ericrbg
    ericrbg committed Mar 6, 2024
    Configuration menu
    Copy the full SHA
    6528080 View commit details
    Browse the repository at this point in the history

  11. choosify UniformSpace/Cauchy

    @ericrbg
    ericrbg committed Mar 6, 2024
    Configuration menu
    Copy the full SHA
    c3576c0 View commit details
    Browse the repository at this point in the history

  12. we add one back in UniformGroup

    @ericrbg
    ericrbg committed Mar 6, 2024
    Configuration menu
    Copy the full SHA
    7511edb View commit details
    Browse the repository at this point in the history

  13. Closeds bites the dots

    @ericrbg
    ericrbg committed Mar 6, 2024
    Configuration menu
    Copy the full SHA
    c695b24 View commit details
    Browse the repository at this point in the history

  14. add a Classical. in GromovHausdorff

    @ericrbg
    ericrbg committed Mar 6, 2024
    Configuration menu
    Copy the full SHA
    a1b943c View commit details
    Browse the repository at this point in the history

  15. decomposition/jordan

    @ericrbg
    ericrbg committed Mar 6, 2024
    Configuration menu
    Copy the full SHA
    ad9ce32 View commit details
    Browse the repository at this point in the history

  16. Classical.choice -> Nonempty.some

    @ericrbg
    ericrbg committed Mar 6, 2024
    Configuration menu
    Copy the full SHA
    127937b View commit details
    Browse the repository at this point in the history