feat(kernel/kernel_exception.h): change application error messages

Error messages are now of the form:
Error: in application
    foo bar
Argument
    bar
has type
    baz
the expected type is
    baz'
feat(kernel/type_checker_justification.cpp): improve error message for type errors on application.
feat(/kernel/type_checker_justification): add better error messages for type mismatch in application.

Fix formatting, correct primes (broken for testing error messages).
test(*): adjust tests due to changes in the error messages

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

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
doc(examples/lean): adjust examples due to changes in error messages

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
fix(frontends/lean/parser_cmds): update help and error messages
feat(frontends/lean/parser_expr): 'namespaces' have precedence over 'using'

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
feat(frontends/lean): add unary_nat command, it forces Lean to convert numerals into unary encoding using nat::succ and nat::zero

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
fix(tests/lean): adjust some tests affected by recent changes

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
feat(shell): add --deps command line option for displaying the direct dependencies of a .lean file

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
fix(builtin/macros): test whether there is an accidental variable capture in 'obtain' macro applications

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
fix(frontends/lean/parser): add to check ".lean" file

Problem
=======

Consider a case where we have:

    library/standard/nat.lean
    library/standard/int2.lean
    ...

and int2.lean has "import nat".

In the previous version, '--deps' generates

    int2.olean: file 'nat' not found in the LEAN_PATH

because it can't find int2.olean.

Solution
========

Add to check ".lean" file and output "<prefix>.olean" as a dependency.
With it, we have

    int2.olean: ./nat.olean ./macros.lua
feat(frontents/lean/parser_cmds):
Print the type of variables introduced by definition, hypothesis (variable) or proof.
fix(emacs/lean-mode):
Undo some local changes to emacs-mode
feat(kernel/kernel_exception.h): change application error messages

Error messages are now of the form:
Error: in application
    foo bar
Argument
    bar
has type
    baz
the expected type is
    baz'
feat(frontends/python): add python binding using SWIG
checkpoint for hurkens.lean