New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
[Merged by Bors] - chore: update unexpanders #11165
Conversation
lean4#3375 makes it so that unexpanders do not need to handle overapplication.
@PatrickMassot As a delaborator connoisseur, I thought I'd ping you to mention that the unexpander overapplication feature that landed works. I also changed your test. It was checking that |
Yes, I wanted |
bors merge |
lean4#3375 makes it so that unexpanders do not need to handle overapplication.
Pull request successfully merged into master. Build succeeded: |
lean4#3375 makes it so that unexpanders do not need to handle overapplication.
lean4#3375 makes it so that unexpanders do not need to handle overapplication.
lean4#3375 makes it so that unexpanders do not need to handle overapplication.
lean4#3375 makes it so that unexpanders do not need to handle overapplication.
lean4#3375 makes it so that unexpanders do not need to handle overapplication.
lean4#3375 makes it so that unexpanders do not need to handle overapplication.