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.

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

[Merged by Bors] - feat: delete Nat.shiftr and Nat.shiftl #6356

Closed
wants to merge 20 commits into from

Commits on Jul 30, 2023

  1. removed shiftl and shiftr

    mhk119 committed Jul 30, 2023
    Configuration menu
    Copy the full SHA
    b8c1db6 View commit details
    Browse the repository at this point in the history

Commits on Aug 4, 2023

  1. Configuration menu
    Copy the full SHA
    af42dd2 View commit details
    Browse the repository at this point in the history
  2. minor changes

    mhk119 committed Aug 4, 2023
    Configuration menu
    Copy the full SHA
    c6f29aa View commit details
    Browse the repository at this point in the history
  3. brougth back shiftl'

    mhk119 committed Aug 4, 2023
    Configuration menu
    Copy the full SHA
    16cde41 View commit details
    Browse the repository at this point in the history

Commits on Aug 5, 2023

  1. Configuration menu
    Copy the full SHA
    a072dc6 View commit details
    Browse the repository at this point in the history
  2. Configuration menu
    Copy the full SHA
    54c1f0d View commit details
    Browse the repository at this point in the history
  3. fixed remaining files

    mhk119 committed Aug 5, 2023
    Configuration menu
    Copy the full SHA
    ea15870 View commit details
    Browse the repository at this point in the history
  4. Configuration menu
    Copy the full SHA
    a849f10 View commit details
    Browse the repository at this point in the history

Commits on Aug 6, 2023

  1. naming

    mhk119 committed Aug 6, 2023
    Configuration menu
    Copy the full SHA
    6ca7971 View commit details
    Browse the repository at this point in the history
  2. Configuration menu
    Copy the full SHA
    7c4bc98 View commit details
    Browse the repository at this point in the history
  3. fixed some build errors

    mhk119 committed Aug 6, 2023
    Configuration menu
    Copy the full SHA
    c7484d4 View commit details
    Browse the repository at this point in the history
  4. Update Mathlib/Init/Data/Nat/Bitwise.lean

    Co-authored-by: Eric Wieser <wieser.eric@gmail.com>
    mhk119 and eric-wieser committed Aug 6, 2023
    Configuration menu
    Copy the full SHA
    16ce204 View commit details
    Browse the repository at this point in the history
  5. Update Mathlib/Data/Num/Lemmas.lean

    Co-authored-by: Eric Wieser <wieser.eric@gmail.com>
    mhk119 and eric-wieser committed Aug 6, 2023
    Configuration menu
    Copy the full SHA
    e0005a6 View commit details
    Browse the repository at this point in the history
  6. changes based on the review

    mhk119 committed Aug 6, 2023
    Configuration menu
    Copy the full SHA
    77d2ed4 View commit details
    Browse the repository at this point in the history
  7. Configuration menu
    Copy the full SHA
    1b4579a View commit details
    Browse the repository at this point in the history
  8. delete bit_0 and bit_1

    mhk119 committed Aug 6, 2023
    Configuration menu
    Copy the full SHA
    490a0ed View commit details
    Browse the repository at this point in the history

Commits on Aug 7, 2023

  1. swapped order

    mhk119 committed Aug 7, 2023
    Configuration menu
    Copy the full SHA
    73694a5 View commit details
    Browse the repository at this point in the history

Commits on Aug 21, 2023

  1. fix lemma name

    eric-wieser committed Aug 21, 2023
    Configuration menu
    Copy the full SHA
    955a9a7 View commit details
    Browse the repository at this point in the history
  2. nolint

    eric-wieser committed Aug 21, 2023
    Configuration menu
    Copy the full SHA
    04e9677 View commit details
    Browse the repository at this point in the history

Commits on Aug 25, 2023

  1. Configuration menu
    Copy the full SHA
    4695dd5 View commit details
    Browse the repository at this point in the history