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] - chore(*): bump to lean 3.47.0 #16252

Closed
wants to merge 14 commits into from
Closed

[Merged by Bors] - chore(*): bump to lean 3.47.0 #16252

wants to merge 14 commits into from

Commits on Aug 25, 2022

  1. chore(*): bump to lean 3.47.0

    @digama0
    digama0 committed Aug 25, 2022
    Configuration menu
    Copy the full SHA
    6f63eac View commit details
    Browse the repository at this point in the history

Commits on Aug 26, 2022

  1. dot notation fix

    @kmill
    kmill committed Aug 26, 2022
    Configuration menu
    Copy the full SHA
    78a3f4a View commit details
    Browse the repository at this point in the history

  2. line length lint

    @kmill
    kmill committed Aug 26, 2022
    Configuration menu
    Copy the full SHA
    d0c31dc View commit details
    Browse the repository at this point in the history

  3. more fixes, merge with kyle's changes

    @digama0
    digama0 committed Aug 26, 2022
    Configuration menu
    Copy the full SHA
    b881408 View commit details
    Browse the repository at this point in the history

  4. add localized docs

    @digama0
    digama0 committed Aug 26, 2022
    Configuration menu
    Copy the full SHA
    4385d67 View commit details
    Browse the repository at this point in the history

  5. Merge remote-tracking branch 'origin/master' into notation_name

    @digama0
    digama0 committed Aug 26, 2022
    Configuration menu
    Copy the full SHA
    f683dd3 View commit details
    Browse the repository at this point in the history

  6. fix

    @digama0
    digama0 committed Aug 26, 2022
    Configuration menu
    Copy the full SHA
    991b347 View commit details
    Browse the repository at this point in the history

  7. fix

    @digama0
    digama0 committed Aug 26, 2022
    Configuration menu
    Copy the full SHA
    2aa66ff View commit details
    Browse the repository at this point in the history

  8. fix

    @digama0
    digama0 committed Aug 26, 2022
    Configuration menu
    Copy the full SHA
    1f4b6c4 View commit details
    Browse the repository at this point in the history

  9. fix

    @digama0
    digama0 committed Aug 26, 2022
    Configuration menu
    Copy the full SHA
    b09ea74 View commit details
    Browse the repository at this point in the history

Commits on Aug 28, 2022

  1. fix tests

    @digama0
    digama0 committed Aug 28, 2022
    Configuration menu
    Copy the full SHA
    94ff308 View commit details
    Browse the repository at this point in the history

  2. fix lint

    @digama0
    digama0 committed Aug 28, 2022
    Configuration menu
    Copy the full SHA
    5acc335 View commit details
    Browse the repository at this point in the history

Commits on Aug 29, 2022

  1. Update src/analysis/inner_product_space/basic.lean 

    Co-authored-by: mcdoll <moritz.doll@googlemail.com>
    @digama0 @mcdoll
    digama0 and mcdoll committed Aug 29, 2022
    Configuration menu
    Copy the full SHA
    ee73749 View commit details
    Browse the repository at this point in the history

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

    @digama0
    digama0 committed Aug 29, 2022
    Configuration menu
    Copy the full SHA
    8d83421 View commit details
    Browse the repository at this point in the history