[Merged by Bors] - chore: to_additive adds instances #678
Conversation
Mathlib/Tactic/ToAdditive.lean
Outdated
| /-- foo -/ | ||
| def copyInstanceAttribute (src tgt : Name) : CoreM Unit := do | ||
| if (← isInstance src) then | ||
| addInstance tgt AttributeKind.global 1000 |>.run' |
There was a problem hiding this comment.
Ideally this would also copy the priority, can we add a todo note here for this?
There was a problem hiding this comment.
This is true and it is not totally trivial, because there are some nice features instances still missing in Core. But I will have a look at that later.
|
Oops I still this is still WIP, so sorry if i just commented something that was already on your mind |
|
It does not work yet and I don't really know why. I somewhat suspect that the instances are registered after the monad in |
|
@alexjbest now your complaints are valid. I've tried and did not make any meaningful progress and I asked on zulip. |
|
Yes, I've also tried this and agree there is missing API (this is why I mentioned adding a TODO rather than implementing it here). I think its probably preferable to merge this for now and improve it later. |
|
Do we need to add some links in the source code to zulip discussions and/or Lean 4 issues asking for this extra API? It would be nice to leave some breadcrumbs here. |
|
Added an issue in Lean 4: leanprover/lean4#1878 |
|
bors merge |
semorrison
added
ready-to-merge
|
Pull request successfully merged into master. Build succeeded:
|
bors
bot
changed the title
No description provided.