feat(util/name): expose is_list_name function

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
feat(library/kernel_bindings): allow a list of level params/globals to be provided to declarations (instead of a list of names)

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
feat(kernel/formatter): prefix metavars with '?' and local vars with '!' in the simple formatter

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

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
test(lua): add constraint generation test when type checking with metavars

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
feat(library/kernel_bindings): add sugar for creating Let expressions from Lua

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
feat(library/kernel_bindings): add let field accessors in the Lua API

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
fix(kernel/expr): bug in m_free_var_range let-expr field

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
test(lua): unit tests for let expressions

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
refactor(library): remove dead files

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
feat(kernel/expr): add is_contextual binder info

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
refactor(kernel/replace_visitor): remove context from replace_visitor

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
refactor(kernel): move mk_tele_pi to expr.h, and rename it mk_pi

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
feat(kernel/formatter): print binder_info in simple formater

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
fix(kernel/type_checker): the type checker cache was not taking into account binder information

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
feat(library/kernel_bindings): expose is_bi_equal predicate in the Lua API

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