chore(emacs/lean-mode): remove lean-tab function
feat(emacs): implement non-blocking communication

The key idea is to pass a continuation function when we call
lean-server-send-cmd function. The passed continuation function is
called by lean-server-event-handler. Until the buffer is ready, the
event handler will be called in interval (lean-server-retry-time, 0.1
sec by default). When we have 'NAY' for INFO command, it will re-send
INFO commands to lean-server until we have one without 'NAY'.

Close #123
feat(emacs/lean-server): support SHOW and VALID

Implement lean-server-show and lean-server-valid functions.

Close #116
feat(emacs/lean-info): add coercion and stale in type info

Close #124
feat(emacs): use lexical scope for lean-info and lean-server
fix(tests/lean/interactive/in4): adjust test

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
feat(emacs/lean-option): show the current value of an option

close #125
refactor(library): add type_util module, and move get_expect_num_args to it

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
feat(frontends/lean/server): add FINDG command (find declarations that can be used to fill a placeholder)

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
feat(frontends/lean): improve COERCION info

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
doc(doc/server): update server documentation

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
feat(library/data/category.lean): add very basic category theory
feat(library/data) add vectors and elimination of false to type
feat(library/data/category.lean)
feat(library/data/category.lean): more experimenting with local instances
feat(library/data/vector.lean) Add basic information about vectors