test(util/lazy_list): add simple lazy_list example

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
refactor(kernel/constraint): simplify constraint interface, and add choice constraint

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
refactor(kernel/abstract): add abstract_locals, and remove abstract_p

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
feat(library/kernel_bindings): expose methods substitution::for_each_expr and substitution::for_each_level in the Lua API

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
refactor(kernel/type_checker): simplify replace constraint_handler with closure

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
feat(library): add unifier module skeleton

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
feat(kernel/metavar): collect unassigned metavariables while instantiating

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
feat(kernel/type_checker): add type_checker::is_def_eq method that takes a justification as argument

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
fix(kernel/converter): add temporary fix, we need to be able to backtrack constraints

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
feat(library/unifier): add unify_fn skeleton

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
feat(library/unifier): add unify_fn skeleton