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>
fix(library/io_state): bug in the io_state Lua bindings

This commit also includes a new test that exposes the problem.
The options in the io_state object were being lost.

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
feat(frontends/lean): macro definition using Lua

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

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
feat(frontends/lean/parser): propagate position information to expressions created by macro implemented in Lua

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
feat(frontends/lean/parser): change show-expression binder name

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

The elaborator was failing in the following scenario:
- Failing constraint of the form
     ctx |- ?m1 =:= ?m2
where
     ?m2 is assigned to ?m1,
     and ?m1 is unassigned.

has_metavar(?m2, ?m1) returns true, and a cycle is incorrectly reported.

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
feat(library/elaborator): only expand definitions that are not marked as hidden

The elaborator produces better proof terms. This is particularly important when we have to prove the remaining holes using tactics.
For example, in one of the tests, the elaborator was producing the sub-expression

 (λ x : N, if ((λ x::1 : N, if (P a x x::1) ⊥ ⊤) == (λ x : N, ⊤)) ⊥ ⊤)

After, this commit it produces

 (λ x : N, ¬ ∀ x::1 : N, ¬ P a x x::1)

The expressions above are definitionally equal, but the second is easier to work with.

Question: do we really need hidden definitions?
Perhaps, we can use only the opaque flag.

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
feat(kernel/environment): add set_opaque method

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
feat(util/sexpr/options): add is_eqp predicate for options

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
feat(kernel/type_checker): use expression before normalization in the unification constraints generated by the typechecker

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>