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: have/let linter #12190

Closed
wants to merge 25 commits into from
Closed

[Merged by Bors] - feat: have/let linter #12190

wants to merge 25 commits into from

Commits on Apr 16, 2024

  1. feat: have/let linter

    @adomani
    adomani committed Apr 16, 2024
    Configuration menu
    Copy the full SHA
    aaa9d84 View commit details
    Browse the repository at this point in the history

  2. add imports

    @adomani
    adomani committed Apr 16, 2024
    Configuration menu
    Copy the full SHA
    30280a5 View commit details
    Browse the repository at this point in the history

Commits on Apr 17, 2024

  1. Eric's MetaM run

    @adomani
    adomani committed Apr 17, 2024
    Configuration menu
    Copy the full SHA
    e25f2e2 View commit details
    Browse the repository at this point in the history

  2. Add a period to the linter message

    @adomani
    adomani committed Apr 17, 2024
    Configuration menu
    Copy the full SHA
    09cd667 View commit details
    Browse the repository at this point in the history

  3. lint multiple introduced hypotheses

    @adomani
    adomani committed Apr 17, 2024
    Configuration menu
    Copy the full SHA
    5bbe4aa View commit details
    Browse the repository at this point in the history

  4. haveLet linter only complains with noise

    @adomani
    adomani committed Apr 17, 2024
    Configuration menu
    Copy the full SHA
    98dbefc View commit details
    Browse the repository at this point in the history

  5. import at bottom and shake

    @adomani
    adomani committed Apr 17, 2024
    Configuration menu
    Copy the full SHA
    7a4e089 View commit details
    Browse the repository at this point in the history

Commits on Apr 19, 2024

  1. Remove exclusions

    @adomani
    adomani committed Apr 19, 2024
    Configuration menu
    Copy the full SHA
    8dbc7fd View commit details
    Browse the repository at this point in the history

  2. linter option is Nat instead of Bool

    @adomani
    adomani committed Apr 19, 2024
    Configuration menu
    Copy the full SHA
    0f74c28 View commit details
    Browse the repository at this point in the history

  3. reduce imports

    @adomani
    adomani committed Apr 19, 2024
    Configuration menu
    Copy the full SHA
    27bc724 View commit details
    Browse the repository at this point in the history

  4. module docs

    @adomani
    adomani committed Apr 19, 2024
    Configuration menu
    Copy the full SHA
    8a9dbec View commit details
    Browse the repository at this point in the history

Commits on May 9, 2024

  1. Merge branch 'master' into adomani/have_let_linter_only

    @adomani
    adomani authored May 9, 2024
    Configuration menu
    Copy the full SHA
    159c6e3 View commit details
    Browse the repository at this point in the history

  2. Update HaveLetLinter.lean

    @adomani
    adomani authored May 9, 2024
    Configuration menu
    Copy the full SHA
    c7566c4 View commit details
    Browse the repository at this point in the history

  3. silence test

    @adomani
    adomani committed May 9, 2024
    Configuration menu
    Copy the full SHA
    3345288 View commit details
    Browse the repository at this point in the history

Commits on May 20, 2024

  1. Merge remote-tracking branch 'origin/master' into adomani/have_let_li… 

    …nter_only
    @adomani
    adomani committed May 20, 2024
    Configuration menu
    Copy the full SHA
    d7241ab View commit details
    Browse the repository at this point in the history

Commits on May 26, 2024

  1. Merge remote-tracking branch 'origin/master' into adomani/have_let_li… 

    …nter_only
    @adomani
    adomani committed May 26, 2024
    Configuration menu
    Copy the full SHA
    160e2b8 View commit details
    Browse the repository at this point in the history

  2. move linter to Linter dir

    @adomani
    adomani committed May 26, 2024
    Configuration menu
    Copy the full SHA
    10937ef View commit details
    Browse the repository at this point in the history

Commits on Jun 17, 2024

  1. Merge remote-tracking branch 'origin/master' into adomani/have_let_li… 

    …nter_only
    @adomani
    adomani committed Jun 17, 2024
    Configuration menu
    Copy the full SHA
    9724831 View commit details
    Browse the repository at this point in the history

  2. unreported, reduce imports

    @adomani
    adomani committed Jun 17, 2024
    Configuration menu
    Copy the full SHA
    06a9d69 View commit details
    Browse the repository at this point in the history

  3. import linter in linter.lean

    @adomani
    adomani committed Jun 17, 2024
    Configuration menu
    Copy the full SHA
    4bd7535 View commit details
    Browse the repository at this point in the history

Commits on Aug 6, 2024

  1. Merge branch 'master' into adomani/have_let_linter_only

    @adomani
    adomani committed Aug 6, 2024
    Configuration menu
    Copy the full SHA
    a085a6b View commit details
    Browse the repository at this point in the history

  2. Jon's comments from review, reduce imports, logging option

    @adomani
    adomani committed Aug 6, 2024
    Configuration menu
    Copy the full SHA
    c23b907 View commit details
    Browse the repository at this point in the history

  3. update tests

    @adomani
    adomani committed Aug 6, 2024
    Configuration menu
    Copy the full SHA
    4c359f2 View commit details
    Browse the repository at this point in the history

  4. Apply suggestions from code review 

    Co-authored-by: Jon Eugster <[email protected]>
    @adomani @joneugster
    adomani and joneugster authored Aug 6, 2024
    Configuration menu
    Copy the full SHA
    d99a922 View commit details
    Browse the repository at this point in the history

  5. Merge branch 'adomani/have_let_linter_only' of github.com:leanprover-… 

    …community/mathlib4 into adomani/have_let_linter_only
    @adomani
    adomani committed Aug 6, 2024
    Configuration menu
    Copy the full SHA
    94894a9 View commit details
    Browse the repository at this point in the history