-
Notifications
You must be signed in to change notification settings - Fork 415
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
feat: detail error message about invalid mutual blocks #2949
Conversation
Thanks for your contribution! Please make sure to follow our Commit Convention. |
|
@odanoburu are you ready for this to be reviewed? It’s still marked as a draft and no The change looks good; it would be good to have a test file that exercises this. Do you want to do that? |
Detail error message to prevent user confusion as in this [Zulip message](https://leanprover.zulipchat.com/#narrow/stream/113489-new-members/topic/Matching.20on.20prop/near/341456011). Instead of just saying ‘invalid mutual block’, explain what a mutual block may contain.
Oh, that’s annoying. I got notifications from github about the new commit, but not that this PR was actually un-drafted. Glad I looked :-) |
I should have left a message, but I feared my rebasing and force-pushing and title changing had already produced too much noise. Sorry about that! |
Not at all your fault, no worries. This is just me getting used to the reviewer side of the workflow. |
To prevent user confusion as in this Zulip message