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>
checkpoint