chore(Data): rename setOf to Set.ofPred#41507
Conversation
This is in prevision of making `Set` a one-field structure. `ofPred` will then be the constructor.
YaelDillies
changed the title
setOf to Set.ofPred`setOf to Set.ofPred
PR summary 5f06fbf1f8Import changes for modified filesNo significant changes to the import graph Import changes for all files
|
YaelDillies
added
t-data
themathqueen
left a comment
themathqueen
left a comment
There was a problem hiding this comment.
Don't think there's a need for both Generated by: and Assisted by:, either one suffices, I think
|
Note that this conflicts with #39110, namely the naming |
|
#39110 is doing eps of the required work. I have the whole refactor building locally. |
The former is an informal description of how I used LLM tools. The latter is in a machine-readable format that follows the Linux kernel contribution convention. |
|
I think merging the small bit will help the review & merge effort (compared to a +3k PR), but I should first fix any incompatibilities with your full PR (and also solve conflicts on my side so that you don't get any). Does it not? |
I doubt so, because your small bits are going against what I am doing in #41506. But don't worry I am going to extract the fixes that can be made on master 😉 |
|
@SnirBroshi, I don't think you should waste time on trying to make that PR more compatible with these (it's far more work than you think, the full PR is huge). Your PR should've been merged 2 months ago (but Yury got busy, I'm assuming), but now with these new PRs, I'm not so sure anymore. I haven't checked, but I think the same stuff is basically in Yaël's PR anyway? Anyway, I think this PR would be easier to review than the rest since it's just a renaming PR. I'll set aside an hour of review time to do this later when it's fully ready. |
| /-lemma autEmbedding_range : | ||
| Set.range (autEmbedding F) = | ||
| ⋂ (f : Arrow C), { a | F.map f.hom ≫ (a f.right).hom = (a f.left).hom ≫ F.map f.hom } := by | ||
| ext a | ||
| simp only [Set.mem_range, id_obj, Set.mem_iInter, Set.mem_setOf_eq] | ||
| simp only [Set.mem_range, id_obj, Set.mem_iInter, Set.mem_ofPred_eq] | ||
| refine ⟨fun ⟨σ, h⟩ i ↦ h.symm ▸ σ.hom.naturality i.hom, fun h ↦ ?_⟩ | ||
| · use NatIso.ofComponents a (fun {X Y} f ↦ h ⟨X, Y, f⟩) | ||
| rfl-/ |
There was a problem hiding this comment.
do you know why this is commented out?
There was a problem hiding this comment.
No clue, but probably out of scope to touch it in this PR?
There was a problem hiding this comment.
Yeah, definitely out of scope
| @@ -258,6 +258,9 @@ def abbreviationDict : Std.HashMap String String := .ofList [ | |||
|
|
|||
| ("neTop", "NeBot"), | |||
| ("decidableSucc", "DecidablePred"), | |||
| -- `Set.ofPred` is not dual to `Set.ofSucc` | |||
There was a problem hiding this comment.
It doesn't exist and that's the point. If you don't add the line below (which we can't see here, please make multiline comments!), then to_dual tries translating ofPred to ofSucc.
themathqueen
added
the
awaiting-author
|
Hey, could you also rename |
YaelDillies
removed
the
awaiting-author
| -- `Set.ofPred` is not dual to `Set.ofSucc` | ||
| ("ofSucc", "OfPred"), | ||
| ("setOfSucc", "SetOfPred"), |
There was a problem hiding this comment.
Sorry for not making a multiline comment before.
Anyway, I see. Let's keep this comment unresolved for other reviewers (especially because I don't fully understand this).
|
I think there are some things to fix outside of mathlib btw, in |
3 participants
This is in prevision of making
Seta one-field structure.ofPredwill then be the constructor.Generated by Claude Opus then reviewed line-by-line by myself.
Assisted-by: Claude Opus 4.8