[Merged by Bors] - refactor: replace some @foo _ _ _ _ _ ... by named arguments
#8702
Conversation
grunweg
added
the
awaiting-review
|
I presume this is awaiting review, hence marking as such. Sorry if this isn't. |
grunweg
changed the title
@foo _ _ _ _ _ ...@foo _ _ _ _ _ ... by named arguments
|
I just pushed a comment addressing my comments, and replacing a few more calls. Happy to move that to a separate PR/feel free to revert. |
|
!bench |
|
Here are the benchmark results for commit 045db19. Benchmark Metric Change
==================================
+ open Mathlib task-clock -7.1% |
winstonyin
removed
the
awaiting-review
|
!bench |
|
Here are the benchmark results for commit 28f5b2c. |
There was a problem hiding this comment.
I am not convinced by any of the changes you did to the category theory library. The rest looks good however.
Can you do one of the following?
- Drop the changes to the category theory library
- Move the changes to the category theory library to a new PR
- Replace the changes to the category theory library by ones that don't involve naming instance arguments
I will swiftly merge this PR once you've done one of the three options. I have a preference for 1 and 2 since it ensures most of your changes get in quickly.
| @@ -253,7 +253,7 @@ instance transferNatTransSelf_symm_iso (f : R₁ ⟶ R₂) [IsIso f] : | |||
| then `f` is an isomorphism. | |||
| The converse is given in `transferNatTransSelf_iso`. | |||
| -/ | |||
| theorem transferNatTransSelf_of_iso (f : L₂ ⟶ L₁) [IsIso (transferNatTransSelf adj₁ adj₂ f)] : | |||
| theorem transferNatTransSelf_of_iso (f : L₂ ⟶ L₁) [i : IsIso (transferNatTransSelf adj₁ adj₂ f)] : | |||
There was a problem hiding this comment.
I'm not fully convinced by the "Let's name an instance argument only because I want to mention it as a named argument later". Instance arguments should usually not be named, and quite definitely not be fed in explicitly.
Can you fix the call site in a way that doesn't involve feeding the instance explicitly, and revert the naming of this instance argument?
There was a problem hiding this comment.
Agreed. You should be able to use letI / haveI to feed instances instead of named arguments or @. (In rare situations when you need to feed non-defeq instances of exactly the same typeclass, you do need @. If you need to feed an instance that conflicts with an existing instance you might do attribute [-instance] existing_instance in.)
There was a problem hiding this comment.
I only added i because frobeniusMorphism_iso_of_expComparison_iso in CategoryTheory/Closed/Functor already had a named type class argument i before this PR. Should that (and a bunch more) be there as well?
letI and haveI don't always work, such as in this case, for reasons I don't understand.
I'll revert these sorts of changes within CategoryTheory for now, in any case.
There was a problem hiding this comment.
I think the named typeclass arguments are here to be used within the declaration itself, in place of an unwiedly long ‹type of the instance assumption› (although I do happen to prefer the latter over the former). What you're doing in contrast is to refer to the name outside of the declaration, which is more brittle and not something I've seen anywhere else.
There was a problem hiding this comment.
I see. Anyway, those changes have been reverted. Thanks for looking at this. I won't add any more changes, so it's ready to be reviewed.
winstonyin
added
the
awaiting-review
|
🚀 Pull request has been placed on the maintainer queue by YaelDillies. |
|
bors merge |
github-actions
bot
added
ready-to-merge
Using Lean4's named arguments, we manage to remove a few hard-to-read explicit function calls `@foo _ _ _ _ _ ...` which used to be necessary in Lean3. Occasionally, this results in slightly longer code. The benefit of named arguments is readability, as well as to reduce the brittleness of the code when the argument order is changed. Co-authored-by: Michael Rothgang <rothgami@math.hu-berlin.de>
|
Build failed (retrying...): |
Using Lean4's named arguments, we manage to remove a few hard-to-read explicit function calls `@foo _ _ _ _ _ ...` which used to be necessary in Lean3. Occasionally, this results in slightly longer code. The benefit of named arguments is readability, as well as to reduce the brittleness of the code when the argument order is changed. Co-authored-by: Michael Rothgang <rothgami@math.hu-berlin.de>
|
Pull request successfully merged into master. Build succeeded: |
mathlib-bors
bot
changed the title
@foo _ _ _ _ _ ... by named arguments@foo _ _ _ _ _ ... by named arguments
Using Lean4's named arguments, we manage to remove a few hard-to-read explicit function calls `@foo _ _ _ _ _ ...` which used to be necessary in Lean3. Occasionally, this results in slightly longer code. The benefit of named arguments is readability, as well as to reduce the brittleness of the code when the argument order is changed. Co-authored-by: Michael Rothgang <rothgami@math.hu-berlin.de>
Using Lean4's named arguments, we manage to remove a few hard-to-read explicit function calls
@foo _ _ _ _ _ ...which used to be necessary in Lean3.Occasionally, this results in slightly longer code. The benefit of named arguments is readability, as well as to reduce the brittleness of the code when the argument order is changed.