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 fin_cases #437

Closed
wants to merge 44 commits into from
Closed

[Merged by Bors] - feat: port fin_cases #437

wants to merge 44 commits into from

Commits on Sep 19, 2022

  1. initial attempt

    @semorrison
    semorrison committed Sep 19, 2022
    Configuration menu
    Copy the full SHA
    4407717 View commit details
    Browse the repository at this point in the history

  2. @(...)

    @semorrison
    semorrison committed Sep 19, 2022
    Configuration menu
    Copy the full SHA
    450a51d View commit details
    Browse the repository at this point in the history

  3. elabAsElim fix

    @semorrison
    semorrison committed Sep 19, 2022
    Configuration menu
    Copy the full SHA
    149ba9a View commit details
    Browse the repository at this point in the history

  4. more progress

    @semorrison
    semorrison committed Sep 19, 2022
    Configuration menu
    Copy the full SHA
    eae4e99 View commit details
    Browse the repository at this point in the history

  5. finish

    @semorrison
    semorrison committed Sep 19, 2022
    Configuration menu
    Copy the full SHA
    612a957 View commit details
    Browse the repository at this point in the history

  6. merge

    @semorrison
    semorrison committed Sep 19, 2022
    Configuration menu
    Copy the full SHA
    5e3b12a View commit details
    Browse the repository at this point in the history

  7. add missing file

    @semorrison
    semorrison committed Sep 19, 2022
    Configuration menu
    Copy the full SHA
    64a8518 View commit details
    Browse the repository at this point in the history

  8. long line

    @semorrison
    semorrison committed Sep 19, 2022
    Configuration menu
    Copy the full SHA
    32b95bd View commit details
    Browse the repository at this point in the history

  9. long line

    @semorrison
    semorrison committed Sep 19, 2022
    Configuration menu
    Copy the full SHA
    4c2341f View commit details
    Browse the repository at this point in the history

Commits on Sep 20, 2022

  1. linting

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

  2. copy from other PR

    @semorrison
    semorrison committed Sep 20, 2022
    Configuration menu
    Copy the full SHA
    8ce2505 View commit details
    Browse the repository at this point in the history

  3. .

    @semorrison
    semorrison committed Sep 20, 2022
    Configuration menu
    Copy the full SHA
    cb6462c View commit details
    Browse the repository at this point in the history

  4. .

    @semorrison
    semorrison committed Sep 20, 2022
    Configuration menu
    Copy the full SHA
    5399838 View commit details
    Browse the repository at this point in the history

  5. lint

    @semorrison
    semorrison committed Sep 20, 2022
    Configuration menu
    Copy the full SHA
    1e6cf7e View commit details
    Browse the repository at this point in the history

  6. .

    @semorrison
    semorrison committed Sep 20, 2022
    Configuration menu
    Copy the full SHA
    3826ff3 View commit details
    Browse the repository at this point in the history

  7. Merge remote-tracking branch 'origin/master' into semorrison/fintype_fin

    @semorrison
    semorrison committed Sep 20, 2022
    Configuration menu
    Copy the full SHA
    5fb5e8a View commit details
    Browse the repository at this point in the history

  8. more

    @semorrison
    semorrison committed Sep 20, 2022
    Configuration menu
    Copy the full SHA
    7faf824 View commit details
    Browse the repository at this point in the history

Commits on Sep 21, 2022

  1. .

    @semorrison
    semorrison committed Sep 21, 2022
    Configuration menu
    Copy the full SHA
    8d384c2 View commit details
    Browse the repository at this point in the history

  2. finish constructing Fintype (Fin n)

    @semorrison
    semorrison committed Sep 21, 2022
    Configuration menu
    Copy the full SHA
    498c9b9 View commit details
    Browse the repository at this point in the history

  3. linting

    @semorrison
    semorrison committed Sep 21, 2022
    Configuration menu
    Copy the full SHA
    143b861 View commit details
    Browse the repository at this point in the history

  4. linting

    @semorrison
    semorrison committed Sep 21, 2022
    Configuration menu
    Copy the full SHA
    c11b823 View commit details
    Browse the repository at this point in the history

  5. long lines

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

  6. cleanup

    @semorrison
    semorrison committed Sep 21, 2022
    Configuration menu
    Copy the full SHA
    edf1063 View commit details
    Browse the repository at this point in the history

  7. surely we can automate...

    @semorrison
    semorrison committed Sep 21, 2022
    Configuration menu
    Copy the full SHA
    5472b31 View commit details
    Browse the repository at this point in the history

  8. Merge branch 'semorrison/fintype_fin' into semorrison/fin_cases

    @semorrison
    semorrison committed Sep 21, 2022
    Configuration menu
    Copy the full SHA
    0f7bb85 View commit details
    Browse the repository at this point in the history

  9. copy tests from mathlib3

    @semorrison
    semorrison committed Sep 21, 2022
    Configuration menu
    Copy the full SHA
    d664f40 View commit details
    Browse the repository at this point in the history

Commits on Sep 23, 2022

  1. minimal implementation

    @semorrison
    semorrison committed Sep 23, 2022
    Configuration menu
    Copy the full SHA
    0fd61be View commit details
    Browse the repository at this point in the history

  2. merge

    @semorrison
    semorrison committed Sep 23, 2022
    Configuration menu
    Copy the full SHA
    eff6ad3 View commit details
    Browse the repository at this point in the history

  3. merge

    @semorrison
    semorrison committed Sep 23, 2022
    Configuration menu
    Copy the full SHA
    7643623 View commit details
    Browse the repository at this point in the history

  4. Merge branch 'semorrison/fintype_fin' into semorrison/fin_cases

    @semorrison
    semorrison committed Sep 23, 2022
    Configuration menu
    Copy the full SHA
    94fa9c2 View commit details
    Browse the repository at this point in the history

  5. merge

    @semorrison
    semorrison committed Sep 23, 2022
    Configuration menu
    Copy the full SHA
    9a7a783 View commit details
    Browse the repository at this point in the history

  6. merge

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

  7. Merge branch 'semorrison/fintype_fin' into semorrison/fin_cases

    @semorrison
    semorrison committed Sep 23, 2022
    Configuration menu
    Copy the full SHA
    02f4f99 View commit details
    Browse the repository at this point in the history

  8. style

    @semorrison
    semorrison committed Sep 23, 2022
    Configuration menu
    Copy the full SHA
    722c9f5 View commit details
    Browse the repository at this point in the history

  9. Merge branch 'semorrison/fintype_fin' into semorrison/fin_cases

    @semorrison
    semorrison committed Sep 23, 2022
    Configuration menu
    Copy the full SHA
    d05944d View commit details
    Browse the repository at this point in the history

  10. include files

    @semorrison
    semorrison committed Sep 23, 2022
    Configuration menu
    Copy the full SHA
    874f761 View commit details
    Browse the repository at this point in the history

  11. documenting changes

    @semorrison
    semorrison committed Sep 23, 2022
    Configuration menu
    Copy the full SHA
    e454555 View commit details
    Browse the repository at this point in the history

Commits on Oct 8, 2022

  1. Merge remote-tracking branch 'origin/master' into semorrison/fin_cases

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

  2. fix

    @semorrison
    semorrison committed Oct 8, 2022
    Configuration menu
    Copy the full SHA
    246b83f View commit details
    Browse the repository at this point in the history

Commits on Oct 18, 2022

  1. cleanup

    @digama0
    digama0 committed Oct 18, 2022
    Configuration menu
    Copy the full SHA
    efcd541 View commit details
    Browse the repository at this point in the history

  2. Merge remote-tracking branch 'origin/master' into semorrison/fin_cases

    @semorrison
    semorrison committed Oct 18, 2022
    Configuration menu
    Copy the full SHA
    353338e View commit details
    Browse the repository at this point in the history

  3. fix example, change in syntax when called with multiple hypotheses

    @semorrison
    semorrison committed Oct 18, 2022
    Configuration menu
    Copy the full SHA
    3a119c6 View commit details
    Browse the repository at this point in the history

  4. fix

    @semorrison
    semorrison committed Oct 18, 2022
    Configuration menu
    Copy the full SHA
    c724d06 View commit details
    Browse the repository at this point in the history

  5. if cases fails, don't catch the error

    @semorrison
    semorrison committed Oct 18, 2022
    Configuration menu
    Copy the full SHA
    73117da View commit details
    Browse the repository at this point in the history