chore: adaptations for lean4#12325 (classDefReducibility)#195
Open
kim-em wants to merge 11 commits intonightly-testing-2026-03-02from
Open
chore: adaptations for lean4#12325 (classDefReducibility)#195kim-em wants to merge 11 commits intonightly-testing-2026-03-02from
kim-em wants to merge 11 commits intonightly-testing-2026-03-02from
Conversation
Add `@[implicit_reducible]` to class-typed `def`s where safe, and disable the warning with `set_option warn.classDefReducibility false in` where adding the attribute causes downstream breakage. Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>
The new toolchain version of lean4#12325 exempts `Setoid` from the classDefReducibility warning, so these suppressions are no longer needed. Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>
Author
|
!radar |
kim-em
changed the base branch from
nightly-testing
to
nightly-testing-2026-03-02
Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>
Author
|
!radar |
|
Benchmark results for d6d02d2 against 6ef7a9d are in! @kim-em
No significant changes detected. |
Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>
sgouezel
reviewed
Mar 6, 2026
|
|
||
| set_option backward.isDefEq.respectTransparency false in | ||
| /-- Any ring with a `ZMod p`-module structure can be upgraded to a `ZMod p`-algebra. Not an | ||
| @[implicit_reducible] |
There was a problem hiding this comment.
Suggested change
| @[implicit_reducible] |
| variable (K) | ||
|
|
||
| /-- `CSA` equipped with Brauer Equivalence is indeed a setoid. -/ | ||
| @[implicit_reducible] |
There was a problem hiding this comment.
Suggested change
| @[implicit_reducible] |
| /-- The setoid given by the equivalence relation `Zigzag`. A quotient for this | ||
| setoid is a connected component of the category. | ||
| -/ | ||
| @[implicit_reducible] |
There was a problem hiding this comment.
Suggested change
| @[implicit_reducible] |
|
|
||
| /-- Two vertices are related in the zigzag setoid if there is a | ||
| zigzag of arrows from one to the other. -/ | ||
| @[implicit_reducible] |
There was a problem hiding this comment.
Suggested change
| @[implicit_reducible] |
| intro i j; obtain ⟨p, _⟩ := h i j; exact ⟨p⟩ | ||
|
|
||
| /-- Equivalence relation identifying vertices connected by directed paths in both directions. -/ | ||
| @[implicit_reducible] |
There was a problem hiding this comment.
Suggested change
| @[implicit_reducible] |
| @@ -471,6 +471,7 @@ end Preconnected | |||
|
|
|||
| section connectedComponentSetoid | |||
| /-- The setoid of connected components of a topological space -/ | |||
| @[implicit_reducible] | |||
There was a problem hiding this comment.
Suggested change
| @[implicit_reducible] |
| @@ -99,6 +99,7 @@ theorem Joined.inv {G : Type*} [Inv G] [TopologicalSpace G] [ContinuousInv G] | |||
| variable (X) | |||
|
|
|||
| /-- The setoid corresponding the equivalence relation of being joined by a continuous path. -/ | |||
| @[implicit_reducible] | |||
There was a problem hiding this comment.
Suggested change
| @[implicit_reducible] |
| @@ -231,6 +231,7 @@ def specializationPreorder : Preorder X := | |||
| lt := fun x y => y ⤳ x ∧ ¬x ⤳ y } | |||
|
|
|||
| /-- A `setoid` version of `Inseparable`, used to define the `SeparationQuotient`. -/ | |||
| @[implicit_reducible] | |||
There was a problem hiding this comment.
Suggested change
| @[implicit_reducible] |
| @@ -447,6 +447,7 @@ theorem ordConnected_setOf_eball_subset (x : α) (s : Set α) : OrdConnected { r | |||
| ⟨fun _ _ _ h₁ _ h₂ => (eball_subset_eball h₂.2).trans h₁⟩ | |||
|
|
|||
| /-- Relation “two points are at a finite edistance” is an equivalence relation. -/ | |||
| @[implicit_reducible] | |||
There was a problem hiding this comment.
Suggested change
| @[implicit_reducible] |
| @@ -404,6 +404,7 @@ section | |||
| variable (X) | |||
|
|
|||
| /-- The smallest equivalence relation on a topological space giving a T2 quotient. -/ | |||
| @[implicit_reducible] | |||
There was a problem hiding this comment.
Suggested change
| @[implicit_reducible] |
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
3 participants
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 adds
@[implicit_reducible]to class-typeddefs where safe, and disables theclassDefReducibilitywarning where adding the attribute causes downstream breakage, for leanprover/lean4#12325.🤖 Prepared with Claude Code