feat(library/basic_thms): add Refute theorem

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
feat(library/basic_thms): add ExistsElim theorem

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
feat(library/basic_thms): simplify DoubleNegElim

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
fix(kernel): incorrect use of scoped_map

This commit also adds a new test that exposes the problem.
The scoped_map should not be used for caching values in the normalizer and type_checker. When we extend the context, the meaning of all variables is modified (we are essentially performing a lift). So, the values stored in the cache are not correct in the new context.

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
fix(library/type_inferer): another incorrect use of scoped_map

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
test(tests/lean): add ExistsElim test

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
feat(library/elaborator): do not create trivial constraints of the form 'ctx |- t =:= t'

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
feat(kernel/printer): include de Bruijn index in the debug printer

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
fix(library/elaborator): missing condition

The elaborator was missing solutions because of the missing condition at is_simple_ho_match.

This commit also adds a new test that exposes the problem.

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
fix(examples/lean/tactic_in_lua): try to make sure the example works when using LuaJIT

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
fix(library/elaborator): bug in process_meta_app

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
fix(kernel/normalizer): bug in Let normalization

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
fix(kernel/normalizer): avoid svalue hack, use 'semantic attachments' for implementing closures, include context in the closure

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
fix(kernel/builtin): make sure the if-then-else semantic attachment is not a simplifier

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

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
feat(kernel/replace_fn): non-recursive replace_fn

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
feat(kernel/normalizer): avoid unnecessary creation of closures for n-ary functions

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
feat(kernel/replace_fn): add template replace that captures commonly used pattern

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
fix(kernel/normalizer): compilation problem with clang++

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
feat(util/name_map): add template alias

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