feat(frontends/lean): add let-expr pretty printer, reduce default indentation to 2

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

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
feat(frontends/lean/pp_options): remove the 'lean.' prefix

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
fix(kernel/level): is_geq predicate

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
feat(frontends/lean): use the same universe in declarations such as (A B : Type)

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
feat(frontends/lean): add Type' as notation for Type.{_+1}

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
feat(kernel/level): improve universe level normalization procedure

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
feat(frontends/lean): improve 'check' command when used inside sections

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
fix(frontends/lean/pp): purify procedure for local names

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
test(tests/lean/run): add more universe tests

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
feat(frontends/lean/pp): add option for displaying fully qualified names

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
test(tests/lean/run): add nested let-expr test

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
refactor(kernel/formatter): add formatter_factory, and simplify formatter interface

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
fix(kernel/expr_eq_fn): take local pp name into account when annotations are considered in the equality test

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
refactor(library/tactic/goal): remove redundance, goal pp method was duplicating some of the functionality provided by the pretty printer

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

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

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
fix(tests/lean): define LEAN_PATH in tests scripts

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
chore(tests/lean): reactivate config.lean

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

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