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(algebra/order/group/defs): split file #17787

Closed
wants to merge 10 commits into from
Closed

[Merged by Bors] - chore(algebra/order/group/defs): split file #17787

wants to merge 10 commits into from

Commits on Dec 2, 2022

  1. chore(algebra/order/group/defs): split file

    @semorrison
    semorrison committed Dec 2, 2022
    Configuration menu
    Copy the full SHA
    0935db6 View commit details
    Browse the repository at this point in the history

  2. fix downstream imports

    @semorrison
    semorrison committed Dec 2, 2022
    Configuration menu
    Copy the full SHA
    5ddae9b View commit details
    Browse the repository at this point in the history

  3. more splits

    @semorrison
    semorrison committed Dec 2, 2022
    Configuration menu
    Copy the full SHA
    dc7c91c View commit details
    Browse the repository at this point in the history

  4. fixes

    @semorrison
    semorrison committed Dec 2, 2022
    Configuration menu
    Copy the full SHA
    c529995 View commit details
    Browse the repository at this point in the history

  5. add assert_not_exists

    @semorrison
    semorrison committed Dec 2, 2022
    Configuration menu
    Copy the full SHA
    fa01945 View commit details
    Browse the repository at this point in the history

  6. fix downstream import

    @semorrison
    semorrison committed Dec 2, 2022
    Configuration menu
    Copy the full SHA
    8f83d79 View commit details
    Browse the repository at this point in the history

  7. Apply suggestions from code review 

    Co-authored-by: Eric Wieser <wieser.eric@gmail.com>
    @semorrison @eric-wieser
    semorrison and eric-wieser committed Dec 2, 2022
    Configuration menu
    Copy the full SHA
    1ab09a5 View commit details
    Browse the repository at this point in the history

  8. remove attribute added for debugging

    @semorrison
    semorrison committed Dec 2, 2022
    Configuration menu
    Copy the full SHA
    22de4d5 View commit details
    Browse the repository at this point in the history

  9. Merge branch 'order_group_split' of github.com:leanprover-community/m… 

    …athlib into order_group_split
    @semorrison
    semorrison committed Dec 2, 2022
    Configuration menu
    Copy the full SHA
    731740d View commit details
    Browse the repository at this point in the history

  10. long line

    @semorrison
    semorrison committed Dec 2, 2022
    Configuration menu
    Copy the full SHA
    2e4c821 View commit details
    Browse the repository at this point in the history