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.

Sign up for GitHub

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

Jump to bottom

change #9952

Closed

mattrobball wants to merge 1 commit into master from mrb/reducible_toAlg

Collaborator

mattrobball commented Jan 24, 2024

No description provided.


          change

d0f505a

Collaborator Author

mattrobball commented Jan 24, 2024

!bench

Member

eric-wieser commented Jan 24, 2024

I'm very confused as to why this makes CI fail

Collaborator Author

mattrobball commented Jan 24, 2024

One needs an extra rfl. Give me a second on the other

Collaborator

leanprover-bot commented Jan 24, 2024

Here are the benchmark results for commit d0f505a.
The entire run failed.
Found no significant differences.

Collaborator Author

mattrobball commented Jan 24, 2024

I give up on this for the night. I think #9949 is fine to merge as is.

mattrobball closed this

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet