diff --git a/src/frontends/lean/CMakeLists.txt b/src/frontends/lean/CMakeLists.txt
index 0bc1c762f..f40f93f1d 100644
--- a/src/frontends/lean/CMakeLists.txt
+++ b/src/frontends/lean/CMakeLists.txt
@@ -1,2 +1,3 @@
-add_library(lean_frontend lean_frontend.cpp lean_operator_info.cpp lean_scanner.cpp lean_parser.cpp lean_pp.cpp lean_notation.cpp)
+add_library(lean_frontend lean_frontend.cpp lean_operator_info.cpp lean_scanner.cpp lean_parser.cpp lean_pp.cpp
+  lean_notation.cpp lean_elaborator.cpp lean_elaborator_exception.cpp)
 target_link_libraries(lean_frontend ${LEAN_LIBS})
diff --git a/src/library/elaborator.cpp b/src/frontends/lean/lean_elaborator.cpp
similarity index 98%
rename from src/library/elaborator.cpp
rename to src/frontends/lean/lean_elaborator.cpp
index 3f14fd627..a55f0eb11 100644
--- a/src/library/elaborator.cpp
+++ b/src/frontends/lean/lean_elaborator.cpp
@@ -5,7 +5,6 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Author: Leonardo de Moura
 */
 #include <deque>
-#include "elaborator.h"
 #include "normalize.h"
 #include "metavar.h"
 #include "printer.h"
@@ -17,7 +16,9 @@ Author: Leonardo de Moura
 #include "replace.h"
 #include "expr_pair.h"
 #include "flet.h"
-#include "elaborator_exception.h"
+#include "lean_frontend.h"
+#include "lean_elaborator.h"
+#include "lean_elaborator_exception.h"
 
 namespace lean {
 static name g_choice_name(name(name(name(0u), "library"), "choice"));
@@ -78,6 +79,7 @@ class elaborator::imp {
     typedef std::deque<constraint>    constraint_queue;
     typedef std::vector<metavar_info> metavars;
 
+    frontend  const &   m_frontend;
     environment const & m_env;
     name_set const *    m_available_defs;
     elaborator const *  m_owner;
@@ -626,10 +628,11 @@ class elaborator::imp {
     }
 
 public:
-    imp(environment const & env, name_set const * defs):
-        m_env(env),
+    imp(frontend const & fe, name_set const * defs):
+        m_frontend(fe),
+        m_env(fe.get_environment()),
         m_available_defs(defs),
-        m_normalizer(env) {
+        m_normalizer(m_env) {
         m_interrupted = false;
         m_owner = nullptr;
     }
@@ -713,7 +716,7 @@ public:
         return r;
     }
 };
-elaborator::elaborator(environment const & env):m_ptr(new imp(env, nullptr)) {}
+elaborator::elaborator(frontend const & fe):m_ptr(new imp(fe, nullptr)) {}
 elaborator::~elaborator() {}
 expr elaborator::operator()(expr const & e) { return (*m_ptr)(e, *this); }
 expr const & elaborator::get_original(expr const & e) const { return m_ptr->get_original(e); }
diff --git a/src/library/elaborator.h b/src/frontends/lean/lean_elaborator.h
similarity index 96%
rename from src/library/elaborator.h
rename to src/frontends/lean/lean_elaborator.h
index 980d11e28..96464eac6 100644
--- a/src/library/elaborator.h
+++ b/src/frontends/lean/lean_elaborator.h
@@ -10,6 +10,7 @@ Author: Leonardo de Moura
 #include "formatter.h"
 
 namespace lean {
+class frontend;
 /**
    \brief Expression elaborator, it is responsible for "filling" holes
    in terms left by the user. This is the main module resposible for computing
@@ -20,7 +21,7 @@ class elaborator {
     std::shared_ptr<imp> m_ptr;
     static void print(imp * ptr);
 public:
-    explicit elaborator(environment const & env);
+    explicit elaborator(frontend const & fe);
     ~elaborator();
 
     expr operator()(expr const & e);
diff --git a/src/frontends/lean/lean_elaborator_exception.cpp b/src/frontends/lean/lean_elaborator_exception.cpp
new file mode 100644
index 000000000..48aa855e4
--- /dev/null
+++ b/src/frontends/lean/lean_elaborator_exception.cpp
@@ -0,0 +1,32 @@
+/*
+Copyright (c) 2013 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+
+Author: Leonardo de Moura
+*/
+#include "lean_elaborator_exception.h"
+#include "lean_elaborator.h"
+
+namespace lean {
+format pp(formatter fmt, elaborator_exception const & ex, options const & opts) {
+    unsigned indent = get_pp_indent(opts);
+    format expr_f = fmt(ex.get_context(), ex.get_expr(), false, opts);
+    format elb_f  = ex.get_elaborator().pp(fmt, opts);
+    return format({format(ex.what()), space(), format("at term"),
+                nest(indent, compose(line(), expr_f)),
+                line(), format("Elaborator state"),
+                nest(indent, compose(line(), elb_f))});
+}
+
+regular const & operator<<(regular const & out, elaborator_exception const & ex) {
+    options const & opts = out.m_state.get_options();
+    out.m_state.get_regular_channel().get_stream() << mk_pair(pp(out.m_state.get_formatter(), ex, opts), opts);
+    return out;
+}
+
+diagnostic const & operator<<(diagnostic const & out, elaborator_exception const & ex) {
+    options const & opts = out.m_state.get_options();
+    out.m_state.get_diagnostic_channel().get_stream() << mk_pair(pp(out.m_state.get_formatter(), ex, opts), opts);
+    return out;
+}
+}
diff --git a/src/library/elaborator_exception.h b/src/frontends/lean/lean_elaborator_exception.h
similarity index 88%
rename from src/library/elaborator_exception.h
rename to src/frontends/lean/lean_elaborator_exception.h
index 025fd0cc1..4d327b6b7 100644
--- a/src/library/elaborator_exception.h
+++ b/src/frontends/lean/lean_elaborator_exception.h
@@ -5,8 +5,9 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Author: Leonardo de Moura
 */
 #pragma once
-#include "elaborator.h"
+#include "lean_elaborator.h"
 #include "kernel_exception.h"
+#include "state.h"
 
 namespace lean {
 /**
@@ -53,4 +54,8 @@ public:
     unification_type_mismatch_exception(elaborator const & elb, context const & ctx, expr const & s):elaborator_exception(elb, ctx, s) {}
     virtual char const * what() const noexcept { return "type mismatch during term elaboration"; }
 };
+
+format pp(formatter fmt, elaborator_exception const & ex, options const & opts);
+regular const & operator<<(regular const & out, elaborator_exception const & ex);
+diagnostic const & operator<<(diagnostic const & out, elaborator_exception const & ex);
 }
diff --git a/src/frontends/lean/lean_parser.cpp b/src/frontends/lean/lean_parser.cpp
index 6a16493c1..9cf074169 100644
--- a/src/frontends/lean/lean_parser.cpp
+++ b/src/frontends/lean/lean_parser.cpp
@@ -18,10 +18,10 @@ Author: Leonardo de Moura
 #include "expr_maps.h"
 #include "sstream.h"
 #include "kernel_exception.h"
-#include "elaborator_exception.h"
 #include "metavar.h"
-#include "elaborator.h"
 #include "lean_frontend.h"
+#include "lean_elaborator.h"
+#include "lean_elaborator_exception.h"
 #include "lean_parser.h"
 #include "lean_scanner.h"
 #include "lean_notation.h"
diff --git a/src/library/CMakeLists.txt b/src/library/CMakeLists.txt
index ddf0e427f..cefce227c 100644
--- a/src/library/CMakeLists.txt
+++ b/src/library/CMakeLists.txt
@@ -1,4 +1,4 @@
 add_library(library basic_thms.cpp deep_copy.cpp max_sharing.cpp
   toplevel.cpp printer.cpp formatter.cpp context_to_lambda.cpp
-  state.cpp metavar.cpp elaborator.cpp update_expr.cpp)
+  state.cpp metavar.cpp update_expr.cpp)
 target_link_libraries(library ${LEAN_LIBS})
diff --git a/src/library/formatter.cpp b/src/library/formatter.cpp
index b5d201ebd..19939df7e 100644
--- a/src/library/formatter.cpp
+++ b/src/library/formatter.cpp
@@ -8,8 +8,6 @@ Author: Leonardo de Moura
 #include "formatter.h"
 #include "printer.h"
 #include "kernel_exception.h"
-#include "elaborator_exception.h"
-#include "elaborator.h"
 
 namespace lean {
 class simple_formatter_cell : public formatter_cell {
@@ -79,14 +77,4 @@ format formatter::operator()(kernel_exception const & ex, options const & opts)
         return format(ex.what());
     }
 }
-
-format formatter::operator()(elaborator_exception const & ex, options const & opts) {
-    unsigned indent = get_pp_indent(opts);
-    format expr_f = operator()(ex.get_context(), ex.get_expr(), false, opts);
-    format elb_f  = ex.get_elaborator().pp(*this, opts);
-    return format({format(ex.what()), space(), format("at term"),
-                nest(indent, compose(line(), expr_f)),
-                line(), format("Elaborator state"),
-                nest(indent, compose(line(), elb_f))});
-}
 }
diff --git a/src/library/formatter.h b/src/library/formatter.h
index 43392bc5b..254eff420 100644
--- a/src/library/formatter.h
+++ b/src/library/formatter.h
@@ -38,7 +38,6 @@ public:
     virtual void set_interrupt(bool flag) {}
 };
 class kernel_exception;
-class elaborator_exception;
 class formatter {
     std::shared_ptr<formatter_cell> m_cell;
 public:
@@ -51,8 +50,6 @@ public:
     format operator()(environment const & env, options const & opts = options()) { return (*m_cell)(env, opts); }
     /** \brief Pretty print a kernel exception using the this formatter */
     format operator()(kernel_exception const & ex, options const & opts = options());
-    /** \brief Pretty print a elaborator exception using the this formatter */
-    format operator()(elaborator_exception const & ex, options const & opts = options());
     void set_interrupt(bool flag) { m_cell->set_interrupt(flag); }
 };
 
diff --git a/src/library/state.h b/src/library/state.h
index c25647347..d35b9928f 100644
--- a/src/library/state.h
+++ b/src/library/state.h
@@ -102,18 +102,6 @@ inline diagnostic const & operator<<(diagnostic const & out, kernel_exception co
     return out;
 }
 
-inline regular const & operator<<(regular const & out, elaborator_exception const & ex) {
-    options const & opts = out.m_state.get_options();
-    out.m_state.get_regular_channel().get_stream() << mk_pair(out.m_state.get_formatter()(ex, opts), opts);
-    return out;
-}
-
-inline diagnostic const & operator<<(diagnostic const & out, elaborator_exception const & ex) {
-    options const & opts = out.m_state.get_options();
-    out.m_state.get_diagnostic_channel().get_stream() << mk_pair(out.m_state.get_formatter()(ex, opts), opts);
-    return out;
-}
-
 template<typename T>
 inline regular const & operator<<(regular const & out, T const & t) {
     out.m_state.get_regular_channel().get_stream() << t;
diff --git a/src/tests/frontends/lean/CMakeLists.txt b/src/tests/frontends/lean/CMakeLists.txt
index 2fe3263ec..c398e5762 100644
--- a/src/tests/frontends/lean/CMakeLists.txt
+++ b/src/tests/frontends/lean/CMakeLists.txt
@@ -10,3 +10,6 @@ add_test(lean_parser ${CMAKE_CURRENT_BINARY_DIR}/lean_parser)
 add_executable(lean_pp lean_pp.cpp)
 target_link_libraries(lean_pp ${EXTRA_LIBS})
 add_test(lean_pp ${CMAKE_CURRENT_BINARY_DIR}/lean_pp)
+add_executable(implicit_args implicit_args.cpp)
+target_link_libraries(implicit_args ${EXTRA_LIBS})
+add_test(implicit_args ${CMAKE_CURRENT_BINARY_DIR}/implicit_args)
diff --git a/src/tests/library/implicit_args.cpp b/src/tests/frontends/lean/implicit_args.cpp
similarity index 94%
rename from src/tests/library/implicit_args.cpp
rename to src/tests/frontends/lean/implicit_args.cpp
index f045c548f..b6eabb398 100644
--- a/src/tests/library/implicit_args.cpp
+++ b/src/tests/frontends/lean/implicit_args.cpp
@@ -6,7 +6,6 @@ Author: Leonardo de Moura
 */
 #include "test.h"
 #include "metavar.h"
-#include "elaborator.h"
 #include "free_vars.h"
 #include "printer.h"
 #include "occurs.h"
@@ -15,16 +14,18 @@ Author: Leonardo de Moura
 #include "basic_thms.h"
 #include "type_check.h"
 #include "kernel_exception.h"
-#include "elaborator_exception.h"
+#include "lean_frontend.h"
+#include "lean_elaborator.h"
+#include "lean_elaborator_exception.h"
 using namespace lean;
 
-expr elaborate(expr const & e, environment const & env) {
+expr elaborate(expr const & e, frontend const & env) {
     elaborator elb(env);
     return elb(e);
 }
 
 // Check elaborator success
-static void success(expr const & e, expr const & expected, environment const & env) {
+static void success(expr const & e, expr const & expected, frontend const & env) {
     std::cout << "\n" << e << "\n------>\n";
     try {
         std::cout << elaborate(e, env) << "\n";
@@ -50,7 +51,7 @@ static void success(expr const & e, expr const & expected, environment const & e
 }
 
 // Check elaborator failure
-static void fails(expr const & e, environment const & env) {
+static void fails(expr const & e, frontend const & env) {
     try {
         expr new_e = elaborate(e, env);
         std::cout << "new_e: " << new_e << std::endl;
@@ -60,7 +61,7 @@ static void fails(expr const & e, environment const & env) {
 }
 
 // Check elaborator partial success (i.e., result still contain some metavariables */
-static void unsolved(expr const & e, environment const & env) {
+static void unsolved(expr const & e, frontend const & env) {
     std::cout << "\n" << e << "\n------>\n" << elaborate(e, env) << "\n";
     lean_assert(has_metavar(elaborate(e, env)));
 }
@@ -68,7 +69,7 @@ static void unsolved(expr const & e, environment const & env) {
 #define _ mk_placholder()
 
 static void tst1() {
-    environment env;
+    frontend env;
     expr A = Const("A");
     expr B = Const("B");
     expr F = Const("F");
@@ -87,7 +88,7 @@ static void tst1() {
 }
 
 static void tst2() {
-    environment env = mk_toplevel();
+    frontend env;
     expr a  = Const("a");
     expr b  = Const("b");
     expr c  = Const("c");
@@ -111,7 +112,7 @@ static void tst2() {
 }
 
 static void tst3() {
-    environment env = mk_toplevel();
+    frontend env;
     expr Nat = Const("Nat");
     env.add_var("Nat", Type());
     env.add_var("vec", Nat >> Type());
@@ -141,7 +142,7 @@ static void tst3() {
 }
 
 static void tst4() {
-    environment env;
+    frontend env;
     expr Nat = Const("Nat");
     env.add_var("Nat", Type());
     expr R   = Const("R");
@@ -163,7 +164,7 @@ static void tst4() {
 }
 
 static void tst5() {
-    environment env;
+    frontend env;
     expr A = Const("A");
     expr B = Const("B");
     expr a = Const("a");
@@ -179,7 +180,7 @@ static void tst5() {
 }
 
 static void tst6() {
-    environment env;
+    frontend env;
     expr lst  = Const("list");
     expr nil  = Const("nil");
     expr cons = Const("cons");
@@ -198,14 +199,14 @@ static void tst6() {
 }
 
 static void tst7() {
-    environment env;
+    frontend env;
     expr x = Const("x");
     expr omega = mk_app(Fun({x,_}, x(x)), Fun({x,_}, x(x)));
     fails(omega, env);
 }
 
 static void tst8() {
-    environment env;
+    frontend env;
     expr B = Const("B");
     expr A = Const("A");
     expr x = Const("x");
@@ -226,7 +227,7 @@ static void tst8() {
 }
 
 static void tst9() {
-    environment env = mk_toplevel();
+    frontend env;
     expr A = Const("A");
     expr B = Const("B");
     expr f = Const("f");
@@ -265,7 +266,7 @@ static void tst9() {
 }
 
 static void tst10() {
-    environment env = mk_toplevel();
+    frontend env;
     expr A = Const("A");
     expr B = Const("B");
     expr C = Const("C");
@@ -290,7 +291,7 @@ static void tst10() {
 
 
 static void tst11() {
-    environment env = mk_toplevel();
+    frontend env;
     expr a  = Const("a");
     expr b  = Const("b");
     expr c  = Const("c");
@@ -310,7 +311,7 @@ static void tst11() {
             Fun({{H1, Eq(a,b)},{H2,Eq(b,c)},{H3,a}},
                 EqTIntro(c, EqMP(a,c,Symm(Bool,c,a,Trans(Bool,c,b,a,Symm(Bool,b,c,H2),Symm(Bool,a,b,H1))), H3))),
             env);
-    environment env2 = mk_toplevel();
+    frontend env2;
     success(Fun({{a,Bool},{b,Bool},{c,Bool},{H1, Eq(a,b)},{H2,Eq(b,c)},{H3,a}},
                 EqTIntro(_, EqMP(_,_,Symm(_,_,_,Trans(_,_,_,_,Symm(_,_,_,H2),Symm(_,_,_,H1))), H3))),
             Fun({{a,Bool},{b,Bool},{c,Bool},{H1, Eq(a,b)},{H2,Eq(b,c)},{H3,a}},
@@ -325,7 +326,7 @@ static void tst11() {
 }
 
 void tst12() {
-    environment env;
+    frontend env;
     expr A  = Const("A");
     expr B  = Const("B");
     expr a  = Const("a");
@@ -338,7 +339,7 @@ void tst12() {
 }
 
 void tst13() {
-    environment env = mk_toplevel();
+    frontend env;
     expr A  = Const("A");
     expr h  = Const("h");
     expr f  = Const("f");
@@ -350,7 +351,7 @@ void tst13() {
 }
 
 void tst14() {
-    environment env = mk_toplevel();
+    frontend env;
     expr R  = Const("R");
     expr A  = Const("A");
     expr r  = Const("r");
diff --git a/src/tests/library/CMakeLists.txt b/src/tests/library/CMakeLists.txt
index b6d713f0a..17647867f 100644
--- a/src/tests/library/CMakeLists.txt
+++ b/src/tests/library/CMakeLists.txt
@@ -1,6 +1,3 @@
-add_executable(implicit_args implicit_args.cpp)
-target_link_libraries(implicit_args ${EXTRA_LIBS})
-add_test(implicit_args ${CMAKE_CURRENT_BINARY_DIR}/implicit_args)
 add_executable(metavar metavar.cpp)
 target_link_libraries(metavar ${EXTRA_LIBS})
 add_test(metavar ${CMAKE_CURRENT_BINARY_DIR}/metavar)