refactor(kernel/converter): converter should fail instead of relying on unification hints for solving a constraint, the hints must be applied by the frontend

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
feat(library): add mk_explicit/is_explicit procedures for '@'-expressions

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
fix(library/choice): avoid assertion violation when Lua API is misused

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
feat(kernel/type_checker): expose app_delayed_justification

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
refactor(kernel): remove 'let'-expressions

We simulate it in the following way:
1- An opaque 'let'-expressions (let x : t := v in b) is encoded as
      ((fun (x : t), b) v)
   We also use a macro (let-macro) to mark this pattern.
   Thus, the pretty-printer knows how to display it correctly.

2- Transparent 'let'-expressions are eagerly expanded by the parser.

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
fix(library/resolve_macro): typo

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
feat(frontends/lean): add frontend elaborator

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
feat(frontends/lean): add frontend elaborator