fix(kernel/formatter): typo

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
feat(kernel): add is_def_eq predicate in the extension_context API

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

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
fix(kernel/formatter): remove unnecessary parenthesis

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
refactor(kernel): revise macro_definition API

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
feat(kernel/kernel_exception): add new auxiliary functions for throwing kernel exceptions

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
refactor(kernel): move delayed_justification to justification.h

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
feat(kernel/justification): add function for creating simple justification objects

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
feat(library): add goodies for binary functions

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

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
fix[kernel/justification.cpp]: style

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
fix(kernel/type_checker): we must use different caches for infer_type and check

The new test tc4.lua exposes the problem being fixed.
We need separate caches otherwise we may mistakenly assume that an expression was already checked by the type checker, while only its type was inferred.

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
feat(library/bin_app): add simpler is_bin_app predicate

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
feat(library/resolve_macro.cpp): add macro to encode propositional resolution proofs compactly

This is also a test for the macro_definition infrastructure that we have in the kernel.

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
test(lua): add tests for resolve macro

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
test(lua): add tests for resolve macro