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 Data.Multiset.Basic #1491

Closed
wants to merge 30 commits into from
Closed

[Merged by Bors] - feat: port Data.Multiset.Basic #1491

wants to merge 30 commits into from

Commits on Jan 11, 2023

  1. feat: port Data.Multiset.Basic

    @jcommelin
    jcommelin committed Jan 11, 2023
    Configuration menu
    Copy the full SHA
    db33bfd View commit details
    Browse the repository at this point in the history

  2. Initial file copy from mathport

    @jcommelin
    jcommelin committed Jan 11, 2023
    Configuration menu
    Copy the full SHA
    93a8bed View commit details
    Browse the repository at this point in the history

  3. Mathbin -> Mathlib; add import to Mathlib.lean

    @jcommelin
    jcommelin committed Jan 11, 2023
    Configuration menu
    Copy the full SHA
    31b371b View commit details
    Browse the repository at this point in the history

  4. tiny start

    @jcommelin
    jcommelin committed Jan 11, 2023
    Configuration menu
    Copy the full SHA
    45cfaeb View commit details
    Browse the repository at this point in the history

  5. fixes

    @jcommelin
    jcommelin committed Jan 11, 2023
    Configuration menu
    Copy the full SHA
    f31679d View commit details
    Browse the repository at this point in the history

Commits on Jan 12, 2023

  1. wip

    @jcommelin
    jcommelin committed Jan 12, 2023
    Configuration menu
    Copy the full SHA
    56bd35e View commit details
    Browse the repository at this point in the history

  2. small fix

    @ChrisHughes24
    ChrisHughes24 committed Jan 12, 2023
    Configuration menu
    Copy the full SHA
    0e9c962 View commit details
    Browse the repository at this point in the history

  3. more fixes

    @ChrisHughes24
    ChrisHughes24 committed Jan 12, 2023
    Configuration menu
    Copy the full SHA
    56d54ba View commit details
    Browse the repository at this point in the history

  4. fixed all red errors

    @jcommelin
    jcommelin committed Jan 12, 2023
    Configuration menu
    Copy the full SHA
    e1ec678 View commit details
    Browse the repository at this point in the history

  5. Update Mathlib.lean

    @Ruben-VandeVelde
    Ruben-VandeVelde committed Jan 12, 2023
    Configuration menu
    Copy the full SHA
    d2926b4 View commit details
    Browse the repository at this point in the history

  6. fix boring warnings

    @rwbarton
    rwbarton committed Jan 12, 2023
    Configuration menu
    Copy the full SHA
    a293406 View commit details
    Browse the repository at this point in the history

  7. fix warnings

    @jcommelin
    jcommelin committed Jan 12, 2023
    Configuration menu
    Copy the full SHA
    50709bd View commit details
    Browse the repository at this point in the history

  8. <= 100 chars

    @qawbecrdtey
    qawbecrdtey committed Jan 12, 2023
    Configuration menu
    Copy the full SHA
    a06298c View commit details
    Browse the repository at this point in the history

  9. long lines

    @jcommelin
    jcommelin committed Jan 12, 2023
    Configuration menu
    Copy the full SHA
    276f484 View commit details
    Browse the repository at this point in the history

  10. Removed 'unusedHavesSuffices' error

    @qawbecrdtey
    qawbecrdtey committed Jan 12, 2023
    Configuration menu
    Copy the full SHA
    db95593 View commit details
    Browse the repository at this point in the history

  11. Update Mathlib/Data/Multiset/Basic.lean 

    Co-authored-by: Ruben Van de Velde <65514131+Ruben-VandeVelde@users.noreply.github.com>
    @jcommelin @Ruben-VandeVelde
    jcommelin and Ruben-VandeVelde committed Jan 12, 2023
    Configuration menu
    Copy the full SHA
    a33cb53 View commit details
    Browse the repository at this point in the history

  12. Update Mathlib/Data/Multiset/Basic.lean 

    Co-authored-by: Ruben Van de Velde <65514131+Ruben-VandeVelde@users.noreply.github.com>
    @jcommelin @Ruben-VandeVelde
    jcommelin and Ruben-VandeVelde committed Jan 12, 2023
    Configuration menu
    Copy the full SHA
    58ff7ef View commit details
    Browse the repository at this point in the history

  13. wip

    @jcommelin
    jcommelin committed Jan 12, 2023
    Configuration menu
    Copy the full SHA
    5930c5f View commit details
    Browse the repository at this point in the history

Commits on Jan 13, 2023

  1. lint

    @jcommelin
    jcommelin committed Jan 13, 2023
    Configuration menu
    Copy the full SHA
    2296d6f View commit details
    Browse the repository at this point in the history

  2. fix final lint issues

    @jcommelin
    jcommelin committed Jan 13, 2023
    Configuration menu
    Copy the full SHA
    3aa30a4 View commit details
    Browse the repository at this point in the history

  3. fix final lint issues

    @jcommelin
    jcommelin committed Jan 13, 2023
    Configuration menu
    Copy the full SHA
    3d68856 View commit details
    Browse the repository at this point in the history

  4. naming and docs fixes

    @jcommelin
    jcommelin committed Jan 13, 2023
    Configuration menu
    Copy the full SHA
    db4f812 View commit details
    Browse the repository at this point in the history

  5. please check these fixes

    @jcommelin
    jcommelin committed Jan 13, 2023
    Configuration menu
    Copy the full SHA
    463207b View commit details
    Browse the repository at this point in the history

  6. fix induction names

    @jcommelin
    jcommelin committed Jan 13, 2023
    Configuration menu
    Copy the full SHA
    e71a483 View commit details
    Browse the repository at this point in the history

  7. move Quot induction principles to new file

    @jcommelin
    jcommelin committed Jan 13, 2023
    Configuration menu
    Copy the full SHA
    561d04e View commit details
    Browse the repository at this point in the history

  8. lint

    @jcommelin
    jcommelin committed Jan 13, 2023
    Configuration menu
    Copy the full SHA
    d571d07 View commit details
    Browse the repository at this point in the history

  9. Update Mathlib/Data/Multiset/Basic.lean 

    Co-authored-by: Ruben Van de Velde <65514131+Ruben-VandeVelde@users.noreply.github.com>
    @jcommelin @Ruben-VandeVelde
    jcommelin and Ruben-VandeVelde committed Jan 13, 2023
    Configuration menu
    Copy the full SHA
    e8ea977 View commit details
    Browse the repository at this point in the history

  10. Apply suggestions from code review 

    Co-authored-by: Ruben Van de Velde <65514131+Ruben-VandeVelde@users.noreply.github.com>
    @jcommelin @Ruben-VandeVelde
    jcommelin and Ruben-VandeVelde committed Jan 13, 2023
    Configuration menu
    Copy the full SHA
    d52133e View commit details
    Browse the repository at this point in the history

  11. Update Mathlib/Data/Multiset/Basic.lean 

    Co-authored-by: Ruben Van de Velde <65514131+Ruben-VandeVelde@users.noreply.github.com>
    @ChrisHughes24 @Ruben-VandeVelde
    ChrisHughes24 and Ruben-VandeVelde committed Jan 13, 2023
    Configuration menu
    Copy the full SHA
    d37f186 View commit details
    Browse the repository at this point in the history

  12. minor changes

    @ChrisHughes24
    ChrisHughes24 committed Jan 13, 2023
    Configuration menu
    Copy the full SHA
    b34da81 View commit details
    Browse the repository at this point in the history