Cleanup

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

src/exprlib/printer.cpp

@@ -171,3 +171,7 @@ std::ostream & operator<<(std::ostream & out, environment const & env) {
     return out;
 }
 }
+void print(lean::expr const & a) { std::cout << a << std::endl; }
+void print(lean::expr const & a, lean::context const & c) { std::cout << mk_pair(a, c) << std::endl; }
+void print(lean::context const & c) { std::cout << c << std::endl; }
+void print(lean::environment const & e) { std::cout << e << std::endl; }

src/kernel/environment.cpp

@@ -7,14 +7,11 @@ Author: Leonardo de Moura
 #include <algorithm>
 #include <vector>
 #include <atomic>
-#include <sstream>
 #include <unordered_map>
 #include "kernel_exception.h"
 #include "environment.h"
 #include "safe_arith.h"
 #include "type_check.h"
-#include "exception.h"
-#include "debug.h"
 
 namespace lean {
 

src/kernel/expr.cpp

@@ -11,10 +11,8 @@ Author: Leonardo de Moura
 #include "free_vars.h"
 #include "expr_sets.h"
 #include "hash.h"
-#include "format.h"
 
 namespace lean {
-
 unsigned hash_args(unsigned size, expr const * args) {
     return hash(size, [&args](unsigned i){ return args[i].hash(); });
 }
@@ -204,4 +202,3 @@ expr copy(expr const & a) {
     return expr();
 }
 }
-void print(lean::expr const & a) { std::cout << a << "\n"; }

src/kernel/expr.h

@@ -387,7 +387,6 @@ struct expr_cell_offset_eqp { unsigned operator()(expr_cell_offset const & p1, e
 
 // =======================================
 // Miscellaneous
-std::ostream & operator<<(std::ostream & out, expr const & a);
 /**
    \brief Wrapper for iterating over application arguments.
 
@@ -468,4 +467,3 @@ template<typename F> expr update_eq(expr const & e, F f) {
 }
 // =======================================
 }
-void print(lean::expr const & a);

src/kernel/free_vars.cpp

@@ -186,5 +186,4 @@ expr lift_free_vars(expr const & e, unsigned d) {
     };
     return replace_fn<decltype(f)>(f)(e);
 }
-
 }

src/kernel/instantiate.h

@@ -21,5 +21,4 @@ inline expr instantiate_with_closed(expr const & e, expr const & s) { return ins
 */
 expr instantiate(expr const & e, unsigned n, expr const * s);
 inline expr instantiate(expr const & e, expr const & s) { return instantiate(e, 1, &s); }
-
 }

src/kernel/type_check.cpp

@@ -12,7 +12,6 @@ Author: Leonardo de Moura
 #include "scoped_map.h"
 #include "builtin.h"
 #include "free_vars.h"
-#include "trace.h"
 
 namespace lean {
 bool is_convertible_core(expr const & expected, expr const & given, environment const & env) {
@@ -58,7 +57,6 @@ struct infer_type_fn {
     }
 
     level infer_universe(expr const & t, context const & ctx) {
-        lean_trace("type_check", tout << "infer universe\n" << t << "\n";);
         expr u = normalize(infer_type(t, ctx), m_env, ctx);
         if (is_type(u))
             return ty_level(u);