Open
Description
We can expect that a large portion of our users have used some similar tool before and, therefore, have an intuition what constructs they should be able to use. However, it can be hard for them to find what is the correct syntax; for example, many tools use different syntax for quantifiers. The Rust compiler has a quite nice job here by giving suggestions and links to the documentation in syntax errors. We should do the same: for example, if we observe the keyword forall
used incorrectly, we could emit a link to the documentation that explains how to use this construct.