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.List.Count #1410

Closed
wants to merge 25 commits into from
Closed

[Merged by Bors] - feat: port Data.List.Count #1410

wants to merge 25 commits into from

Commits on Jan 6, 2023

  1. Initial file copy from mathport

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

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

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

  3. names and capitalization

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

  4. wip

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

  5. wip

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

  6. wip

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

  7. fixes

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

Commits on Jan 7, 2023

  1. fixes

    @semorrison
    semorrison committed Jan 7, 2023
    Configuration menu
    Copy the full SHA
    2ffd48d View commit details
    Browse the repository at this point in the history

  2. Merge remote-tracking branch 'origin/master' into port/Data.List.BigO… 

    …perators.Basic
    @semorrison
    semorrison committed Jan 7, 2023
    Configuration menu
    Copy the full SHA
    3af83dd View commit details
    Browse the repository at this point in the history

  3. long lines

    @semorrison
    semorrison committed Jan 7, 2023
    Configuration menu
    Copy the full SHA
    66a2231 View commit details
    Browse the repository at this point in the history

  4. Initial file copy from mathport

    @zeramorphic
    zeramorphic committed Jan 7, 2023
    Configuration menu
    Copy the full SHA
    dc9ff01 View commit details
    Browse the repository at this point in the history

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

    @zeramorphic
    zeramorphic committed Jan 7, 2023
    Configuration menu
    Copy the full SHA
    a6ef7d6 View commit details
    Browse the repository at this point in the history

  6. Merge remote-tracking branch 'origin/port/Data.List.BigOperators.Basi… 

    …c' into port/Data.List.Count
    @zeramorphic
    zeramorphic committed Jan 7, 2023
    Configuration menu
    Copy the full SHA
    97021c3 View commit details
    Browse the repository at this point in the history

  7. File compiles 

    Signed-off-by: zeramorphic <zeramorphic@proton.me>
    @zeramorphic
    zeramorphic committed Jan 7, 2023
    Configuration menu
    Copy the full SHA
    d6361d2 View commit details
    Browse the repository at this point in the history

  8. Naming fixes, use implicit lambdas 

    Signed-off-by: zeramorphic <zeramorphic@proton.me>
    @zeramorphic
    zeramorphic committed Jan 7, 2023
    Configuration menu
    Copy the full SHA
    b4b6c4d View commit details
    Browse the repository at this point in the history

Commits on Jan 10, 2023

  1. Merge branch 'master' into port/Data.List.Count

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

  2. lint 2/3

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

  3. lint

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

  4. shorten one proof

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

  5. shorten one more proof

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

  6. move theorems about bool to bool

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

  7. restore lemmas about repeat

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

  8. lint fix

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

  9. Apply suggestions from code review 

    Co-authored-by: Johan Commelin <johan@commelin.net>
    @zeramorphic @jcommelin
    zeramorphic and jcommelin committed Jan 10, 2023
    Configuration menu
    Copy the full SHA
    a22772b View commit details
    Browse the repository at this point in the history

  10. Update Mathlib/Data/List/Count.lean

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