-
Notifications
You must be signed in to change notification settings - Fork 47
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
Emit an error when using a law
attribute incorrectly
#904
Comments
Could it make sense to allow adding the attribute to non-trait methods (lemmas)? They could be automatically added to the context whenever the type the method is for is brought into scope. |
That's another way to solve this issue, indeed. I agree that we need an auto-load mechanism for lemmas which are not part of traits. But this poses several questions:
|
Note: laws of traits have a different behavior: they are triggerred by uses of methods of the trait (not of the type). This means that we would have a different bahavior. Is this confusing? |
I agree that the question of inherent laws should be addressed in a second piece of work. Ensuring the 'coherence' of declaration types is more important. |
#[law]
should only be allowed in trait method declarations and when giving an implementation of a law.The text was updated successfully, but these errors were encountered: