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] - feat(simps): improve error messages #4653
Conversation
src/tactic/simps.lean
Outdated
* `@[_simps_str]` is automatically added to structures that have been used in `@[simps]` at least | ||
once. They contain the data of the projections used for this structure by all following | ||
invocations of `@[simps]`. |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
I'm not sure what the referent of They
is in "They contain the data". Could you add a bit more here?
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Better now?
LGTM. I'll |
Thanks for this, this would have definitely saved me the confusion I had on Zulip! |
Co-authored-by: Scott Morrison <scott.morrison@gmail.com>
@semorrison ping |
bors merge |
If a custom projection has a different type than the expected projection, then it will show a more specific error message. Also reflow most long lines Also add some tests
Pull request successfully merged into master. Build succeeded: |
If a custom projection has a different type than the expected projection, then it will show a more specific error message.
Also reflow most long lines
Also add some tests
Not sure what to do with strings of
>100
characters without newline in it.@eric-wieser