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.

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

[Merged by Bors] - feat(algebra/ordered*): more simp lemmas #4359

Closed
wants to merge 14 commits into from

Commits on Oct 2, 2020

  1. Snapshot

    urkud committed Oct 2, 2020
    Configuration menu
    Copy the full SHA
    ff472e3 View commit details
    Browse the repository at this point in the history
  2. More lemmas

    urkud committed Oct 2, 2020
    Configuration menu
    Copy the full SHA
    cca03b0 View commit details
    Browse the repository at this point in the history
  3. Fix

    urkud committed Oct 2, 2020
    Configuration menu
    Copy the full SHA
    80f927a View commit details
    Browse the repository at this point in the history
  4. Fix

    urkud committed Oct 2, 2020
    Configuration menu
    Copy the full SHA
    6250a2a View commit details
    Browse the repository at this point in the history
  5. Fix

    urkud committed Oct 2, 2020
    Configuration menu
    Copy the full SHA
    e3b97f1 View commit details
    Browse the repository at this point in the history
  6. Try to fix lint

    urkud committed Oct 2, 2020
    Configuration menu
    Copy the full SHA
    dfdd2a3 View commit details
    Browse the repository at this point in the history
  7. Fix

    urkud committed Oct 2, 2020
    Configuration menu
    Copy the full SHA
    5e2980b View commit details
    Browse the repository at this point in the history
  8. Configuration menu
    Copy the full SHA
    89cd80f View commit details
    Browse the repository at this point in the history
  9. Remove simp attributes

    urkud committed Oct 2, 2020
    Configuration menu
    Copy the full SHA
    4af4405 View commit details
    Browse the repository at this point in the history
  10. Fix

    urkud committed Oct 2, 2020
    Configuration menu
    Copy the full SHA
    9397365 View commit details
    Browse the repository at this point in the history
  11. Fix

    urkud committed Oct 2, 2020
    Configuration menu
    Copy the full SHA
    c1cb15b View commit details
    Browse the repository at this point in the history
  12. Fix

    urkud committed Oct 2, 2020
    Configuration menu
    Copy the full SHA
    9f3b2ea View commit details
    Browse the repository at this point in the history
  13. Fix

    urkud committed Oct 2, 2020
    Configuration menu
    Copy the full SHA
    1c36c8a View commit details
    Browse the repository at this point in the history

Commits on Oct 3, 2020

  1. Configuration menu
    Copy the full SHA
    3cc3414 View commit details
    Browse the repository at this point in the history