fix: update Grind.CommRing to avoid constructing non-defeq NatCast instance#8161
Merged
fix: update Grind.CommRing to avoid constructing non-defeq NatCast instance#8161
Conversation
5dfded4 to
89299ac
Compare
ghost
pushed a commit
to leanprover-community/batteries
that referenced
this pull request
Apr 29, 2025
ghost
pushed a commit
to leanprover-community/mathlib4
that referenced
this pull request
Apr 29, 2025
|
kim-em
added a commit
to leanprover-community/mathlib4
that referenced
this pull request
Apr 29, 2025
kim-em
added a commit
to leanprover-community/mathlib4
that referenced
this pull request
May 2, 2025
* Trigger CI for leanprover/lean4#7971 * WIP * WIP * WIP * Trigger CI for leanprover/lean4#7971 * Update lean-toolchain for testing leanprover/lean4#7975 * Fix * Trigger CI for leanprover/lean4#7971 * remove adaptation notes * Fix * Fix * chore: bump to nightly-2025-04-16 * revert some stuff * Update lean-toolchain for testing leanprover/lean4#7983 * WIP * Part one * Part two * lake update and fix * Fix * Trigger CI for leanprover/lean4#7983 * Shake * chore: bump to nightly-2025-04-17 * lake update * . * chore: bump to nightly-2025-04-18 * Update lean-toolchain for testing leanprover/lean4#8021 * fix * fix: !bench after Lake path changes (#24143) * fix * fix * chore: bump to nightly-2025-04-19 * Merge master into nightly-testing * temporarirly disable sythorder checking for Grind.IsCharP instance * shake * chore: bump to nightly-2025-04-20 * fix * chore: bump to nightly-2025-04-21 * make fix more robust * fix test * chore: bump to nightly-2025-04-22 * . * sorries * sorries * chore: bump to nightly-2025-04-23 * chore: bump to nightly-2025-04-24 * fix * not there yet * comment out * comment out * chore: bump to nightly-2025-04-25 * bump batteries * more * hacky fix? * add comment * fix lint-style * Fix shake: Parser.parseHeader returns TSyntax instead of Syntax after the new module system * Clean up * Update lean-toolchain for testing leanprover/lean4#8000 * Lake update * Fix * Fix * Fix * Fix * fix to Mathlib/Algebra/Homology/Embedding/Connect.lean * Fix * chore: bump to nightly-2025-04-26 * fix MinImports * Update lean-toolchain for testing leanprover/lean4#8114 * lake update * fix * fixes * fix * fix deprecations * remove accidental files * chore: bump to nightly-2025-04-26 * chore: bump to nightly-2025-04-27 * fixes * cleanup adaptation note * shake --fix * cleanup * . * cleanup * cleanup * cleanup * comments * cleanuo * move batteries back to nightly-testing * fix * fix build hopefully? * fix build hopefully? * chore: bump to nightly-2025-04-28 * Update lean-toolchain for testing leanprover/lean4#8144 * lake update * Fix * fix grind instances * shake * Cleanup * shake * chore: bump to nightly-2025-04-29 * fix * deprecation * Update lean-toolchain for testing leanprover/lean4#8161 * shake * fix GrindInstances * basic test for grind +ring * fixes for leanprover/lean4#8161 * fixes * chore: adaptations for nightly-2025-04-29 * Merge master into nightly-testing * chore: bump to nightly-2025-04-30 * lake update * fix * fix merge * fix merge * Drop a few unnecessary changes * fix test * chore: bump to nightly-2025-05-01 * fix --------- Co-authored-by: leanprover-community-mathlib4-bot <leanprover-community-mathlib4-bot@users.noreply.github.com> Co-authored-by: Markus Himmel <markus@lean-fro.org> Co-authored-by: github-actions <github-actions@github.com> Co-authored-by: Rob23oba <robin.arnez@web.de> Co-authored-by: Sebastian Ullrich <sebasti@nullri.ch> Co-authored-by: Kyle Miller <kmill31415@gmail.com> Co-authored-by: Joël Riou <joel.riou@universite-paris-saclay.fr> Co-authored-by: Ruben Van de Velde <65514131+Ruben-VandeVelde@users.noreply.github.com> Co-authored-by: Johan Commelin <johan@commelin.net>
kim-em
added a commit
to leanprover-community/mathlib4
that referenced
this pull request
May 5, 2025
* chore: bump to nightly-2025-04-16 * revert some stuff * Update lean-toolchain for testing leanprover/lean4#7983 * WIP * Part one * Part two * lake update and fix * Fix * Trigger CI for leanprover/lean4#7983 * Shake * chore: bump to nightly-2025-04-17 * lake update * . * chore: bump to nightly-2025-04-18 * Update lean-toolchain for testing leanprover/lean4#8021 * fix * fix: !bench after Lake path changes (#24143) * fix * fix * chore: bump to nightly-2025-04-19 * Merge master into nightly-testing * temporarirly disable sythorder checking for Grind.IsCharP instance * shake * chore: bump to nightly-2025-04-20 * fix * chore: bump to nightly-2025-04-21 * make fix more robust * fix test * chore: bump to nightly-2025-04-22 * . * sorries * sorries * chore: bump to nightly-2025-04-23 * chore: bump to nightly-2025-04-24 * fix * not there yet * comment out * comment out * chore: bump to nightly-2025-04-25 * bump batteries * more * hacky fix? * add comment * fix lint-style * Fix shake: Parser.parseHeader returns TSyntax instead of Syntax after the new module system * Clean up * Update lean-toolchain for testing leanprover/lean4#8000 * Lake update * Fix * Fix * Fix * Fix * fix to Mathlib/Algebra/Homology/Embedding/Connect.lean * Fix * chore: bump to nightly-2025-04-26 * fix MinImports * Update lean-toolchain for testing leanprover/lean4#8114 * lake update * fix * fixes * fix * fix deprecations * remove accidental files * chore: bump to nightly-2025-04-26 * chore: bump to nightly-2025-04-27 * fixes * cleanup adaptation note * shake --fix * cleanup * . * cleanup * cleanup * cleanup * comments * cleanuo * move batteries back to nightly-testing * fix * fix build hopefully? * fix build hopefully? * chore: bump to nightly-2025-04-28 * Update lean-toolchain for testing leanprover/lean4#8144 * lake update * Fix * fix grind instances * shake * Cleanup * shake * chore: bump to nightly-2025-04-29 * fix * deprecation * Update lean-toolchain for testing leanprover/lean4#8161 * shake * fix GrindInstances * basic test for grind +ring * fixes for leanprover/lean4#8161 * fixes * chore: adaptations for nightly-2025-04-29 * Merge master into nightly-testing * chore: bump to nightly-2025-04-30 * lake update * fix * fix merge * fix merge * Drop a few unnecessary changes * fix test * chore: bump to nightly-2025-05-01 * fix * Merge master into nightly-testing * chore: bump to nightly-2025-05-02 * chore: bump to nightly-2025-05-03 * chore: adaptations for nightly-2025-05-03 --------- Co-authored-by: leanprover-community-mathlib4-bot <leanprover-community-mathlib4-bot@users.noreply.github.com> Co-authored-by: github-actions <github-actions@github.com> Co-authored-by: Rob23oba <robin.arnez@web.de> Co-authored-by: Markus Himmel <markus@lean-fro.org> Co-authored-by: Kim Morrison <kim@tqft.net> Co-authored-by: Sebastian Ullrich <sebasti@nullri.ch> Co-authored-by: Kyle Miller <kmill31415@gmail.com> Co-authored-by: Joël Riou <joel.riou@universite-paris-saclay.fr> Co-authored-by: Ruben Van de Velde <65514131+Ruben-VandeVelde@users.noreply.github.com>
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
1 participant
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
This PR changes
Lean.Grind.CommRingto inline theNatCastinstance (i.e. to be provided by the user) rather than constructing one from the existing data. Without this change we can't construct instances in Mathlib thatgrindcan use.