-
Notifications
You must be signed in to change notification settings - Fork 135
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
Different behaviour when working across different modules #2217
Comments
You need to repeat the |
Maybe the error message could suggest that an infix declaration is missing. This wouldn't be a difficult contribution, I think. Propagating infix declarations when importing modules would be a bit harder. Also, some care is necessary to check that the infix declarations can qualify the operators to disambiguate them when there are multiple definitions in a project. |
Thank you! |
Yeah, the "cannot parse specification" message is of little help. |
Hello. Let's say we have a first module:
and a second module importing previous one
I see the following parsing error concering the +. operator in the lemma declaration:
However, if i put all these definitions inside the same module, there is no problem. How come?
The text was updated successfully, but these errors were encountered: