Emit an error when using a law attribute incorrectly

[jhjourdan]

#[law] should only be allowed in trait method declarations and when giving an implementation of a law.

[dewert99]

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.

[jhjourdan]

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:

• What does "a types is brought into scope" means, exactly?
• Is this really the auto-load mechanism we want? It seems rather weak, I would rather prefer not having to add yet another one if this one is not enough.

[jhjourdan]

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?

[xldenis]

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:

* What does "a types is brought into scope" means, exactly?

* Is this really the auto-load mechanism we want? It seems rather weak, I would rather prefer not having to add yet another one if this one is not enough.

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.