Skip to content

Conversation

@mattrobball
Copy link
Collaborator

No description provided.

@mattrobball
Copy link
Collaborator Author

!bench

@eric-wieser
Copy link
Member

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

@mattrobball
Copy link
Collaborator Author

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

@leanprover-bot
Copy link
Collaborator

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

@mattrobball
Copy link
Collaborator Author

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

@YaelDillies YaelDillies deleted the mrb/reducible_toAlg branch August 12, 2025 05:40
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

4 participants