feat(kernel/inductive): add inductive datatype kernel extension module interface

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
refactor(kernel): add binder structure

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
refactor(kernel): improve names

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
feat(kernel): add telescope instantiate procedure

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
feat(kernel): add telescope abstract procedure

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
feat(util/name): use '.' instead of '::' as hierarchical name separator

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
feat(kernel/expr): attach auxiliary name (for pretty printing) into local constants

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
feat(library/kernel_bindings): improve Pi and Fun Lua APIs, and allow users to provide binder information

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
feat(kernel): add proof irrelevance for classes

We can use this feature to implement proof irrelevance for Identity types.

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
feat(kernel/formatter): make simple_formatter display Type instead of Bool if impredicativity is disabled

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
test(lua): add test simulating HoTT compatible environment

   Type.{0} is predicative
   Type.{0} is proof relevant
   Id       is proof irrelevant
   Path     is proof relevant

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
fix(kernel/abstract): compilation warnining

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
fix(kernel/expr): memory leak introduced today

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
fix(kernel/abstract): bug in abstract for telescopes

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
feat(kernel/inductive): add getters for inductive decls

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
feat(library/kernel_bindings): add Lua API for declaring datatypes

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
feat(library/kernel_bindings): add sugar for level expressions in the Lua API

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
refactor(kernel/inductive): simplify inductive datatype API

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
test(lua): add inductive datatype simple tests

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
test(lean): remove tests using Lean old syntax and kernel

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>