[Merged by Bors] - feat: port Topology.Algebra.GroupCompletion #2637
Conversation
ocfnash
commented
Mar 4, 2023
ocfnash
commented
Mathbin -> Mathlib fix certain import statements move "by" to end of line add import to Mathlib.lean
I'm not completely sure this is the right approach but if it is then it will still be necessary to: * avoid dependence on auto-generated instance names (or better, on instance names at all) * add various 'porting not' comments * [maybe] investigate the failures of `rw_mod_cast`
ocfnash
added
WIP
Explicitly naming two instances to support linking from comments
ocfnash
added
awaiting-review
| /-- Automatic coercion from `α` to its completion. Not always injective. -/ | ||
| instance : CoeTC α (Completion α) := | ||
| ⟨Quotient.mk' ∘ pureCauchy⟩ | ||
| instance : Coe α (Completion α) := |
There was a problem hiding this comment.
Have I done the right thing here?
Before this change, the coercion was being eagerly unfolded and causing the usual problems (e.g., with rewrites).
I note also that the guidance from core regarding CoeTC is that:
Auxiliary class implementing `Coe*`.
Users should generally not implement this directly.
There was a problem hiding this comment.
My imporession is that adding the @[coe] def coe' above is sufficient, and that you don't need this instance at all. But I could be very wrong about that.
There was a problem hiding this comment.
I wasn't clear on this myself but your comment motivated me to look this up!
Based on what I see here I now understand that both the @[coe] and the instance are required. (Of course I also verified that if I remove the instance then the coercions don't work.)
|
bors r+ |
github-actions
bot
added
ready-to-merge
|
Pull request successfully merged into master. Build succeeded: |
bors
bot
changed the title
