fix(library/elaborator): strength elaborator procedure for handling equality and convertability constraints

This commit improves the condition for showing that an equality(and convertability) constraint cannot be solved. A nice consequence is that Lean produces nicer error messages. For example, the error message for unit test elab1.lean is more informative.

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
fix(kernel/type_checker): Pi with metavariables case

The type checker (and type inferer) were not handling correctly Pi expressions where the type universe cannot be established due to the occurrence of metavariables. In this case, a max-constraint is created. The problem is that the domain and body of the Pi are in different contexts. The constrain generated before this commit was incorrect, it could contain a free variable. This commit fix the issue by using the context of the body, and lifting the free variables in the domain by 1.

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
fix(frontends/lean/notation): change the precedence of '->'

It should match the precedence of the implication '=>'.

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
fix(frontends/lean/notation): change the precedence of '->'