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

refactor: make 1 % n reduce without well-founded recursion #4098

Merged
merged 4 commits into from
May 8, 2024
Merged

refactor: make 1 % n reduce without well-founded recursion #4098

merged 4 commits into from
May 8, 2024

Commits on May 7, 2024

  1. refactor: make 1 % n reduce without well-founded recursion 

    this is in preparation for #4061. Once that lands, `1 % 42 = 1` will no
longer hold definitionally (at least not without an ungly `unseal
Nat.modCore in` around). This affects mathlib in a few places,
essentially every time a `1 : Fin (n+1)` literal is written.

So this extends the existing special case for `0 % n = 0` to `1 % n`.
    @nomeata
    nomeata committed May 7, 2024
    Configuration menu
    Copy the full SHA
    90780bb View commit details
    Browse the repository at this point in the history

  2. Update src/Init/Data/Nat/Div.lean

    @nomeata
    nomeata authored May 7, 2024
    Configuration menu
    Copy the full SHA
    d2017ce View commit details
    Browse the repository at this point in the history

  3. Improve modCore_eq_mod

    @nomeata
    nomeata committed May 7, 2024
    Configuration menu
    Copy the full SHA
    7254574 View commit details
    Browse the repository at this point in the history

  4. Unused variable

    @nomeata
    nomeata committed May 7, 2024
    Configuration menu
    Copy the full SHA
    3509232 View commit details
    Browse the repository at this point in the history