feat(kernel): add general purpose 'annotations', they are just a generalization of the 'let'-annotations

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
feat(frontends/lean): improve 'type mismatch' error position, and annotate 'have'-expressions

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
feat(emacs): improve font highlighting in emacs mode

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
fix(frontends/lean/pp): display private 'internal' names in a human readable way

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
feat(frontends/lean/pp): add option for displaying internal names associated with private declarations

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
fix(frontends/lean/decl_cmds): support for section declarations with implicit parameters, they must be tagged with '@' when creating aliases

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
feat(frontends/lean/inductive_cmd): improve notation for declaring 'empty' inductive datatypes

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
refactor(library/standard): cleanup notation

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
fix(library/inductive_unifier_plugin): unification problem failure on problems with inductive datatypes

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
fix(frontends/lean/elaborator): instantiate assigned metavariables before collecting unassigned ones

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
fix(library/unifier): do not let a unification plugin to 'prioritize' a flex-flex constraint, and add missing case

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
fix(library/inductive_unifier_plugin): do not try to solve type incorrect constraints

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
fix(library/unifier): more bugs in the unifier

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
test(tests/lean/run): another test for the unifier

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
fix(library/unifier): fix cryptic error message

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

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

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
feat(util/worker_queue): allow main thread to process tasks while waiting

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
Added a crash test case.
Proved cantor's theorem