feat(frontend/lean/server.cpp): add "-- BEGININFO" header
refactor(kernel/instantiate): add functions instantiate_value_univ_params and instantiate_type_univ_params

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
feat(frontends/lean): remove feature that in declarations such as (A B : Type), forced A and B to be in the same universe

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
refactor(frontends/lean/elaborator): remove m_accumulated and eager metavariable instantiation

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
refactor(frontends/lean/elaborator): remove unnecessary field: m_subst

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
feat(frontends/lean): change 'proof-qed' semantics: no backtracking

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
fix(frontends/lean/server): disable cache, when a definition is reused from the cache, we loose type information, fixes #35

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

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
fix(frontends/lean/scanner): wrong column information produced by scanner

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
fix(tests/lean): adjust tests expected output

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
feat(bin/lmake): add --jobs and --keep-going options
fix(emacs): remove lean-get-this-if-true-or-that
feat(emacs/lean-flycheck): customize checker name and options
feat(emacs): implement lean-show-type
refactor(frontends/lean): rename elaborator_env to elaborator_context

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
fix(frontends/lean/server): crash when INFO is invoked before VISIT/LOAD

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
fix(bin/lmake): remove debugging messages
feat(emacs): show overload information
fix(emacs): add missing 'require'

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
fix(emacs): add and use lean-string-join