[Merged by Bors] - feat: toAdditive to transfer MatcherInfo data#16026
[Merged by Bors] - feat: toAdditive to transfer MatcherInfo data#16026
Conversation
so that printing the definitions shows `match … with` properly, and meta code looking for matchers work. Fixes an item on #1074
PR summary c1a5e8e4ddImport changes for modified filesNo significant changes to the import graph Import changes for all files
Declarations diffNo declarations were harmed in the making of this PR! 🐙 You can run this locally as follows## summary with just the declaration names:
./scripts/declarations_diff.sh <optional_commit>
## more verbose report:
./scripts/declarations_diff.sh long <optional_commit>The doc-module for |
|
Thanks for fixing this! I guess/hope that a few workarounds for this issue can be removed now (search for #1074, item (8)). Would you like to perform this clean-up also? |
I wouldn’t mind if someone else will do that :-) |
|
Never mind, this actually fixes item 7 on the list: I don't see any obvious locations where this would simplify mathlib code. |
|
This is also needed after leanprover/lean4#4154 hits lean master, so if we merge it now then the nightly testing maintainers (@semorrison and @jcommelin) have less work with the next nightly. |
|
Sold! bors merge |
so that printing the definitions shows `match … with` properly, and meta code looking for matchers work. Fixes an item on #1074
|
Pull request successfully merged into master. Build succeeded: |
so that printing the definitions shows `match … with` properly, and meta code looking for matchers work. Fixes an item on #1074
so that printing the definitions shows `match … with` properly, and meta code looking for matchers work. Fixes an item on #1074
so that printing the definitions shows `match … with` properly, and meta code looking for matchers work. Fixes an item on #1074
so that printing the definitions shows
match … withproperly, andmeta code looking for matchers work.
Fixes an item on #1074