feat(frontends/lean): add pretty printer configuration options

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
feat(library/head_map): a simple indexing datastructure

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

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
feat(frontends/lean): allow user to suppress proofs in theorems, and let them be inferred automatically using tactic_hints

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
feat(frontends/lean): allow tactic_hints to be applied when class-instance mechanism fails

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

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
feat(library/tactic/apply_tactic): add option for 'refreshing' universe metavariables in the 'apply' tactic

The new test ../../tests/lean/run/tactic27.lean demonstrates why we need this feature. The tactic 'apply @refl' is actually 'apply @refl.{?l}'. It is used inside of a repeat tactical. Each iteration of the 'repeat' may need to use a different value for ?l. Before this commit, there was not way to say we want a fresh ?l each iteration.

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
fix(library/tactic): avoid 'unknown' message in trace_tac when position information is not available

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

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

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
fix(util/sexpr): nested Lua objects

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
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>