diff --git a/src/frontends/lean/frontend.cpp b/src/frontends/lean/frontend.cpp index d9949658a..628fedb5f 100644 --- a/src/frontends/lean/frontend.cpp +++ b/src/frontends/lean/frontend.cpp @@ -20,6 +20,7 @@ Author: Leonardo de Moura #include "kernel/builtin.h" #include "kernel/io_state.h" #include "library/io_state_stream.h" +#include "library/ite.h" #include "library/expr_pair.h" #include "library/expr_pair_maps.h" #include "library/arith/nat.h" @@ -569,6 +570,7 @@ io_state init_frontend(environment const & env, bool no_kernel) { io_state init_test_frontend(environment const & env) { env->set_trusted_imported(true); io_state ios = init_frontend(env); + import_ite(env, ios); import_int(env, ios); import_real(env, ios); return ios; diff --git a/src/library/kernel_bindings.cpp b/src/library/kernel_bindings.cpp index 7307a434b..389ed7727 100644 --- a/src/library/kernel_bindings.cpp +++ b/src/library/kernel_bindings.cpp @@ -5,6 +5,7 @@ Released under Apache 2.0 license as described in the file LICENSE. Author: Leonardo de Moura */ #include +#include #include "util/sstream.h" #include "util/script_state.h" #include "kernel/expr.h"