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] - feat: port Order.Category.BddOrdCat #4984

Closed
wants to merge 10 commits into from
Closed

[Merged by Bors] - feat: port Order.Category.BddOrdCat #4984

wants to merge 10 commits into from

Commits on Jun 12, 2023

  1. feat: port Order.Category.BddOrd

    @joneugster
    joneugster committed Jun 12, 2023
    Configuration menu
    Copy the full SHA
    c04e629 View commit details
    Browse the repository at this point in the history

  2. Initial file copy from mathport

    @joneugster
    joneugster committed Jun 12, 2023
    Configuration menu
    Copy the full SHA
    43dc068 View commit details
    Browse the repository at this point in the history

  3. automated fixes 

    Mathbin -> Mathlib
fix certain import statements
move "by" to end of line
add import to Mathlib.lean
    @joneugster
    joneugster committed Jun 12, 2023
    Configuration menu
    Copy the full SHA
    ed16c8e View commit details
    Browse the repository at this point in the history

  4. rename file and fix import

    @joneugster
    joneugster committed Jun 12, 2023
    Configuration menu
    Copy the full SHA
    730fd8c View commit details
    Browse the repository at this point in the history

  5. easy fixes

    @joneugster
    joneugster committed Jun 12, 2023
    Configuration menu
    Copy the full SHA
    1c5c68a View commit details
    Browse the repository at this point in the history

  6. partial progress

    @joneugster
    joneugster committed Jun 12, 2023
    Configuration menu
    Copy the full SHA
    fd40e36 View commit details
    Browse the repository at this point in the history

  7. almost there

    @joneugster
    joneugster committed Jun 12, 2023
    Configuration menu
    Copy the full SHA
    6b86df4 View commit details
    Browse the repository at this point in the history

  8. it compiles

    @joneugster
    joneugster committed Jun 12, 2023
    Configuration menu
    Copy the full SHA
    43d46f8 View commit details
    Browse the repository at this point in the history

  9. update Mathlib.lean

    @joneugster
    joneugster committed Jun 12, 2023
    Configuration menu
    Copy the full SHA
    b5b857f View commit details
    Browse the repository at this point in the history

Commits on Jun 13, 2023

  1. minor

    Scott Morrison committed Jun 13, 2023
    Configuration menu
    Copy the full SHA
    18aa216 View commit details
    Browse the repository at this point in the history