chore(library/basic_thms): fix typo in comment

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
fix(frontends/lean/pp): make sure pp and parser are using the same precedences

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
feat(frontends/lean): hide 'explicit' version of objects with implicit arguments

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
feat(frontends/lean): hide builtin object in the 'Show Environment' command

The user can still display builtin objects by using

    Show Environment all

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
fix(kernel/kernel_exception): incorrect pp method

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
fix(kernel/expr): avoid '_' as a binder name, we use '_' as a placeholder in the Lean frontend

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
fix(frontends/lean/parser): parse_type method

The parser had a nasty ambiguity. For example,
    f Type 1
had two possible interpretations
    (f (Type) (1))
or
    (f (Type 1))

To fix this issue, whenever we want to specify a particular universe, we have to precede 'Type' with a parenthesis.
Examples:
    (Type 1)
    (Type U)
    (Type M + 1)

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
fix(frontends/lean/pp): pretty printer for Type

Add parenthesis around Type when it has a universe.

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
feat(frontends/lean): improve coercion manangement

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
test(tests/lean): add new test script that checks if Lean can parse the output produced by its pretty printer

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
test(tests/lean): add new test script that checks if Lean can parse the output produced by its pretty printer