chore: remove dead code

src/library/CMakeLists.txt

@@ -6,7 +6,7 @@ add_library(library OBJECT expr_lt.cpp io_state.cpp
   pp_options.cpp projection.cpp
   aux_recursors.cpp trace.cpp
   type_context.cpp
-  locals.cpp messages.cpp message_builder.cpp check.cpp
+  locals.cpp messages.cpp message_builder.cpp
   profiling.cpp time_task.cpp
   scope_pos_info_provider.cpp formatter.cpp json.cpp
   pos_info_provider.cpp abstract_type_context.cpp)

src/library/check.cpp

@@ -1,30 +0,0 @@
-/*
-Copyright (c) 2017 Microsoft Corporation. All rights reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-
-Author: Leonardo de Moura
-*/
-#include "kernel/expr_sets.h"
-#include "kernel/instantiate.h"
-#include "library/trace.h"
-#include "library/type_context.h"
-
-namespace lean {
-struct check_fn {
-    type_context_old &   m_ctx;
-    expr_set             m_visited;
-public:
-    check_fn(type_context_old & ctx):m_ctx(ctx) {}
-};
-
-void check(type_context_old &, expr const &) {
-    lean_unreachable();
-}
-
-void initialize_check() {
-    register_trace_class("check");
-}
-
-void finalize_check() {
-}
-}

src/library/check.h

@@ -1,20 +0,0 @@
-/*
-Copyright (c) 2017 Microsoft Corporation. All rights reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-
-Author: Leonardo de Moura
-*/
-#pragma once
-#include "library/type_context.h"
-
-namespace lean {
-/* Type check 'e' using the given type context.
-   It throws an exception in case of failure.
-
-   This procedure is use to check the proof-term produced by tactics such as
-   rewrite.
-*/
-void check(type_context_old & ctx, expr const & e);
-void initialize_check();
-void finalize_check();
-}

src/library/init_module.cpp

@@ -16,7 +16,6 @@ Author: Leonardo de Moura
 #include "library/util.h"
 #include "library/pp_options.h"
 #include "library/type_context.h"
-#include "library/check.h"
 #include "library/profiling.h"
 #include "library/time_task.h"
 #include "library/formatter.h"
@@ -49,13 +48,11 @@ void initialize_library_module() {
     initialize_library_util();
     initialize_pp_options();
     initialize_type_context();
-    initialize_check();
     initialize_time_task();
 }
 
 void finalize_library_module() {
     finalize_time_task();
-    finalize_check();
     finalize_type_context();
     finalize_pp_options();
     finalize_library_util();

src/library/type_context.cpp

@@ -26,7 +26,6 @@ Author: Leonardo de Moura
 #include "library/locals.h"
 #include "library/aux_recursors.h"
 #include "library/num.h"
-#include "library/check.h"
 #include "library/time_task.h"
 
 namespace lean {