[Merged by Bors] - chore(*): rename FunLike to DFunLike#9785
[Merged by Bors] - chore(*): rename FunLike to DFunLike#9785Vierkantor wants to merge 9 commits intomasterfrom
FunLike to DFunLike#9785Conversation
This prepares for the introduction of a non-dependent synonym of FunLike, which helps a lot with keeping #8386 readable. This is entirely search-and-replace. The commands that generated this change: ```bash sed -i 's/\bFunLike\b/DFunLike/g' {Archive,Counterexamples,Mathlib,test}/**/*.lean sed -i 's/import Mathlib.Data.DFunLike/import Mathlib.Data.FunLike/g' {Archive,Counterexamples,Mathlib,test}/**/*.lean ```
871dbbd to
4145626
Compare
| /-- Helper instance for when there's too many metavariables to apply `DFunLike.CoeFun` | ||
| directly. -/ | ||
| /- Porting note: Lean gave me `unknown constant 'FunLike.CoeFun'` and says `CoeFun` is a type | ||
| /- Porting note: Lean gave me `unknown constant 'DFunLike.CoeFun'` and says `CoeFun` is a type |
There was a problem hiding this comment.
Do you think editing this porting note is OK?
There was a problem hiding this comment.
Not sure: it would be false as written so probably revert this? Although I suppose the error would involve DFunLike if we ported now, so maybe it's okay. Probably we can delete this instance anyway (after #8386).
| /- Porting note: Lean gave me `unknown constant 'DFunLike.CoeFun'` and says `CoeFun` is a type | |
| /- Porting note: Lean gave me `unknown constant 'FunLike.CoeFun'` and says `CoeFun` is a type |
mattrobball
left a comment
There was a problem hiding this comment.
Quick pass through visible changes in GH UI. Only some naming conventions.
| used for example with `ContinuousLinearMap` or `Matrix`. | ||
| -/ | ||
| structure IsProj {F : Type*} [FunLike F M fun _ => M] (f : F) : Prop where | ||
| structure IsProj {F : Type*} [DFunLike F M fun _ => M] (f : F) : Prop where |
There was a problem hiding this comment.
Should this be dependent? Might be out of scope for this PR
There was a problem hiding this comment.
I'd like to postpone this cleanup after the heavy changes of #8386 have passed.
| This typeclass is primarily for use by homomorphisms like `MonoidHom` and `LinearMap`. | ||
|
|
||
| ## Basic usage of `FunLike` | ||
| ## Basic usage of `DFunLike` |
There was a problem hiding this comment.
Should this entire directory be renamed Mathlib/Data/DFunLike?
There was a problem hiding this comment.
We're going to re-add FunLike in #8386 and pretend it's the main definition (or at least the one most users will care about), so I'd like to keep the current directory name.
| variable {F α β : Sort*} [i : DFunLike F α fun _ ↦ β] | ||
|
|
||
| namespace FunLike | ||
| namespace DFunLike |
There was a problem hiding this comment.
Is the idea right now to still leave this stuff in the DFunLike namespace?
There was a problem hiding this comment.
For now, yes. I would like to eventually have everything in the FunLike namespace (except perhaps anything specialized to the dependent case), but that would require something smarter than a find-and-replace everywhere.
| /-- The type of `⊤`-preserving functions from `α` to `β`. -/ | ||
| structure TopHom (α β : Type*) [Top α] [Top β] where | ||
| /-- The underlying function. The preferred spelling is `FunLike.coe`. -/ | ||
| /-- The underlying function. The preferred spelling is `DFunLike.coe`. -/ |
There was a problem hiding this comment.
Do you think that the preferred spelling will be FunLike.coe again one day? (also the change a few lines later)
There was a problem hiding this comment.
I don't know: coe is a field of the DFunLike structure so it's not quite as easy to rename it as it would be for a plain definition.
Co-authored-by: Eric Wieser <wieser.eric@gmail.com>
Co-authored-by: Kevin Buzzard <k.buzzard@imperial.ac.uk>
Co-authored-by: Kevin Buzzard <k.buzzard@imperial.ac.uk>
|
I decided to rename all the |
|
I think this has had a thorough look-over. I am going to delegate it. If anyone has any more comments, please register them soon. bors-delegate+ |
|
Human error. bors delegate+ |
|
✌️ Vierkantor can now approve this pull request. To approve and merge a pull request, simply reply with |
|
Build passed! I'll merge in a couple hours unless there are any further comments. |
|
I see no objection and no changes relating to bors merge |
This prepares for the introduction of a non-dependent synonym of FunLike, which helps a lot with keeping #8386 readable. This is entirely search-and-replace in [680197f](680197f) combined with manual fixes in [4145626](4145626), [e900597](e900597) and [b8428f8](b8428f8). The commands that generated this change: ```bash sed -i 's/\bFunLike\b/DFunLike/g' {Archive,Counterexamples,Mathlib,test}/**/*.lean sed -i 's/\btoFunLike\b/toDFunLike/g' {Archive,Counterexamples,Mathlib,test}/**/*.lean sed -i 's/import Mathlib.Data.DFunLike/import Mathlib.Data.FunLike/g' {Archive,Counterexamples,Mathlib,test}/**/*.lean sed -i 's/\bHom_FunLike\b/Hom_DFunLike/g' {Archive,Counterexamples,Mathlib,test}/**/*.lean sed -i 's/\binstFunLike\b/instDFunLike/g' {Archive,Counterexamples,Mathlib,test}/**/*.lean sed -i 's/\bfunLike\b/instDFunLike/g' {Archive,Counterexamples,Mathlib,test}/**/*.lean sed -i 's/\btoo many metavariables to apply `fun_like.has_coe_to_fun`/too many metavariables to apply `DFunLike.hasCoeToFun`/g' {Archive,Counterexamples,Mathlib,test}/**/*.lean ``` Co-authored-by: Anne Baanen <Vierkantor@users.noreply.github.com>
|
Pull request successfully merged into master. Build succeeded: |
FunLike to DFunLikeFunLike to DFunLike
This follows up from #9785, which renamed `FunLike` to `DFunLike`, by introducing a new abbreviation `FunLike F α β := DFunLike F α (fun _ => β)`, to make the non-dependent use of `FunLike` easier.
This follows up from #9785, which renamed `FunLike` to `DFunLike`, by introducing a new abbreviation `FunLike F α β := DFunLike F α (fun _ => β)`, to make the non-dependent use of `FunLike` easier. I searched for the pattern `DFunLike.*fun` and `DFunLike.*λ` in all files to replace expressions of the form `DFunLike F α (fun _ => β)` with `FunLike F α β`. I did this everywhere except for `extends` clauses for two reasons: it would conflict with #8386, and more importantly `extends` must directly refer to a structure with no unfolding of `def`s or `abbrev`s.
This prepares for the introduction of a non-dependent synonym of FunLike, which helps a lot with keeping #8386 readable.
This is entirely search-and-replace in 680197f combined with manual fixes in 4145626, e900597 and b8428f8. The commands that generated this change: