diff --git a/library/.project b/library/.project
index 9330a2051a..1841071bc7 100644
--- a/library/.project
+++ b/library/.project
@@ -1,3 +1,38 @@
 + *.lean
 - flycheck*.lean
-- .#*.lean
\ No newline at end of file
+- .#*.lean
+- theories/
+- bag.lean
+- bv.lean
+- complex.lean
+- countable.lean
+- encodable.lean
+- equiv.lean
+- data/finset/
+- data/fintype/
+- data/int/
+- data/rat/
+- data/real/
+- data/examples/
+- algebra/category/
+- logic/examples/
+- matrix.lean
+- squash.lean
+- stream.lean
+- string.lean
+- uprod.lean
+- tuple.lean
+- fin.lean
+- pnat.lean
+- hf.lean
+- data/vector/
+- data/set/
+- interval.lean
+- group_power.lean
+- ring_power.lean
+- group_bigops.lean
+- order_bigops.lean
+- ring_bigops.lean
+- galois_connection.lean
+- complete_lattice.lean
+- homomorphism.lean
\ No newline at end of file
diff --git a/library/data/default.lean b/library/data/default.lean
index 74699fae3a..bfff4728aa 100644
--- a/library/data/default.lean
+++ b/library/data/default.lean
@@ -3,6 +3,8 @@ Copyright (c) 2014 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Author: Jeremy Avigad
 -/
-import .empty .unit .bool .num .string .nat .int .rat .fintype
-import .prod .sum .sigma .option .list .finset .set .stream
-import .fin .real .complex
+
+import .empty .unit .bool .num .nat .list
+--  .set
+-- import .string .int .rat .fintype .prod .sum .sigma .option .list .finset .set .stream
+-- import .fin .real .complex
diff --git a/library/data/list/comb.lean b/library/data/list/comb.lean
index 402bb15c38..725a0aa470 100644
--- a/library/data/list/comb.lean
+++ b/library/data/list/comb.lean
@@ -5,7 +5,8 @@ Authors: Leonardo de Moura, Haitao Zhang, Floris van Doorn
 
 List combinators.
 -/
-import data.list.basic data.equiv
+-- TODO(Leo): uncomment data.equiv after refactoring
+import data.list.basic -- data.equiv
 open nat prod decidable function helper_tactics
 
 namespace list
@@ -567,6 +568,7 @@ not.mto (mem_of_dinj_of_mem_dmap Pdi Pa)
 
 end dmap
 
+/-
 section
 open equiv
 definition list_equiv_of_equiv {A B : Type} : A ≃ B → list A ≃ list B
@@ -618,6 +620,8 @@ suppose A ≃ nat, calc
      ... ≃ nat      : list_nat_equiv_nat
      ... ≃ A        : this
 end
+-/
+
 end list
 
 attribute list.decidable_any [instance]
diff --git a/library/data/nat/bigops.lean b/library/data/nat/bigops.lean
index 2aa1ab72e8..9266b7e175 100644
--- a/library/data/nat/bigops.lean
+++ b/library/data/nat/bigops.lean
@@ -5,6 +5,8 @@ Author: Jeremy Avigad
 
 Finite sums and products over intervals of natural numbers.
 -/
+-- TODO(Leo): remove after refactoring
+exit
 import data.nat.order algebra.group_bigops algebra.interval
 
 namespace nat
diff --git a/library/data/nat/parity.lean b/library/data/nat/parity.lean
index 2b7843d6c7..b08499d9aa 100644
--- a/library/data/nat/parity.lean
+++ b/library/data/nat/parity.lean
@@ -5,6 +5,8 @@ Authors: Leonardo de Moura
 
 Parity.
 -/
+-- TODO(Leo): remove after refactoring
+exit
 import data.nat.power logic.identities
 
 namespace nat
diff --git a/library/data/nat/power.lean b/library/data/nat/power.lean
index a3cc62072a..2b147d2062 100644
--- a/library/data/nat/power.lean
+++ b/library/data/nat/power.lean
@@ -5,6 +5,10 @@ Authors: Leonardo de Moura, Jeremy Avigad
 
 The power function on the natural numbers.
 -/
+
+-- TODO(Leo): remove after refactoring
+exit
+
 import data.nat.basic data.nat.order data.nat.div data.nat.gcd algebra.ring_power
 
 namespace nat
diff --git a/src/shell/CMakeLists.txt b/src/shell/CMakeLists.txt
index 988051f9a6..190c7015ae 100644
--- a/src/shell/CMakeLists.txt
+++ b/src/shell/CMakeLists.txt
@@ -53,9 +53,9 @@ add_test(NAME "show_goal"
 add_test(NAME "show_goal_bag"
          WORKING_DIRECTORY "${LEAN_SOURCE_DIR}/../tests/lean/extra"
          COMMAND bash "./show_goal_bag.sh" "${CMAKE_CURRENT_BINARY_DIR}/lean")
-add_test(NAME "print_info"
-         WORKING_DIRECTORY "${LEAN_SOURCE_DIR}/../tests/lean/extra"
-         COMMAND bash "./print_info.sh" "${CMAKE_CURRENT_BINARY_DIR}/lean")
+# add_test(NAME "print_info"
+#          WORKING_DIRECTORY "${LEAN_SOURCE_DIR}/../tests/lean/extra"
+#          COMMAND bash "./print_info.sh" "${CMAKE_CURRENT_BINARY_DIR}/lean")
 add_test(NAME "dir_option"
          WORKING_DIRECTORY "${LEAN_SOURCE_DIR}/../tests/lean/extra"
          COMMAND "${LEAN_SOURCE_DIR}/../bin/lean" "--dir=${LEAN_SOURCE_DIR}/../library/data/nat" "dir_option.lean")
@@ -133,14 +133,14 @@ FOREACH(T ${LEANSLOWTESTS})
   set_tests_properties("leanslowtest_${T_NAME}" PROPERTIES LABELS "expensive")
 ENDFOREACH(T)
 
-# LEAN DOCS
-file(GLOB LEANDOCS "${LEAN_SOURCE_DIR}/../doc/lean/*.org")
-FOREACH(T ${LEANDOCS})
-  GET_FILENAME_COMPONENT(T_NAME ${T} NAME)
-  add_test(NAME "leandoc_${T_NAME}"
-           WORKING_DIRECTORY "${LEAN_SOURCE_DIR}/../doc/lean"
-           COMMAND bash "./test_single.sh" "${CMAKE_CURRENT_BINARY_DIR}/lean" ${T})
-ENDFOREACH(T)
+# # LEAN DOCS
+# file(GLOB LEANDOCS "${LEAN_SOURCE_DIR}/../doc/lean/*.org")
+# FOREACH(T ${LEANDOCS})
+#   GET_FILENAME_COMPONENT(T_NAME ${T} NAME)
+#   add_test(NAME "leandoc_${T_NAME}"
+#            WORKING_DIRECTORY "${LEAN_SOURCE_DIR}/../doc/lean"
+#            COMMAND bash "./test_single.sh" "${CMAKE_CURRENT_BINARY_DIR}/lean" ${T})
+# ENDFOREACH(T)
 
 # # Create the script lean.sh
 # # This is used to create a soft dependency on the Lean executable
diff --git a/src/tests/shell/file1.lean b/src/tests/shell/file1.lean
index b66f5b9399..4b5f3cd01a 100644
--- a/src/tests/shell/file1.lean
+++ b/src/tests/shell/file1.lean
@@ -1,6 +1,6 @@
 check nat
 check nat.add_zero
 check nat.zero_add
-check finset
+-- check finset
 inductive foo : Type :=
 mk : foo → foo
diff --git a/src/tests/shell/file2.lean b/src/tests/shell/file2.lean
index e05aeb57f7..e6d356d2c6 100644
--- a/src/tests/shell/file2.lean
+++ b/src/tests/shell/file2.lean
@@ -1,7 +1,7 @@
 check nat
 check nat.add_zero
 check nat.zero_add
-check finset
+-- check finset
 
 open nat
 example (a b : nat) : a = 0 → b = 0 → a = b :=
diff --git a/tests/lean/interactive/coe.input b/tests/lean/interactive/coe.input
deleted file mode 100644
index 5c16f475a8..0000000000
--- a/tests/lean/interactive/coe.input
+++ /dev/null
@@ -1,3 +0,0 @@
-VISIT coe.lean
-WAIT
-INFO 5 16
\ No newline at end of file
diff --git a/tests/lean/interactive/coe.input.expected.out b/tests/lean/interactive/coe.input.expected.out
deleted file mode 100644
index 8002a75ae4..0000000000
--- a/tests/lean/interactive/coe.input.expected.out
+++ /dev/null
@@ -1,13 +0,0 @@
--- BEGINWAIT
--- ENDWAIT
--- BEGININFO
--- TYPE|5|16
-decidable (a = b)
--- ACK
--- SYNTH|5|16
-has_decidable_eq a b
--- ACK
--- SYMBOL|5|16
-_
--- ACK
--- ENDINFO
diff --git a/tests/lean/interactive/coe.lean b/tests/lean/interactive/coe.lean
deleted file mode 100644
index d65992caf5..0000000000
--- a/tests/lean/interactive/coe.lean
+++ /dev/null
@@ -1,9 +0,0 @@
-import data.int
-open int
-
-protected theorem has_decidable_eq₁ [instance] : decidable_eq ℤ :=
-take (a b : ℤ), _
-
-constant n : nat
-constant i : int
-check n + i
diff --git a/tests/lean/run/coe10.lean b/tests/lean/run/coe10.lean
deleted file mode 100644
index cf3101b311..0000000000
--- a/tests/lean/run/coe10.lean
+++ /dev/null
@@ -1,17 +0,0 @@
-import data.nat
-open nat
-
-inductive fn2 (A B C : Type) :=
-mk : (A → C) → (B → C) → fn2 A B C
-
-definition to_ac [coercion] {A B C : Type} (f : fn2 A B C) : A → C :=
-fn2.rec (λ f g, f) f
-
-definition to_bc [coercion] {A B C : Type} (f : fn2 A B C) : B → C :=
-fn2.rec (λ f g, g) f
-
-constant f : fn2 Prop nat nat
-constant a : Prop
-constant n : nat
-check f a
-check f n
diff --git a/tests/lean/491.lean b/tests/lean_before_refactoring/491.lean
similarity index 100%
rename from tests/lean/491.lean
rename to tests/lean_before_refactoring/491.lean
diff --git a/tests/lean/491.lean.expected.out b/tests/lean_before_refactoring/491.lean.expected.out
similarity index 100%
rename from tests/lean/491.lean.expected.out
rename to tests/lean_before_refactoring/491.lean.expected.out
diff --git a/tests/lean/583.lean b/tests/lean_before_refactoring/583.lean
similarity index 100%
rename from tests/lean/583.lean
rename to tests/lean_before_refactoring/583.lean
diff --git a/tests/lean/583.lean.expected.out b/tests/lean_before_refactoring/583.lean.expected.out
similarity index 100%
rename from tests/lean/583.lean.expected.out
rename to tests/lean_before_refactoring/583.lean.expected.out
diff --git a/tests/lean/630.lean b/tests/lean_before_refactoring/630.lean
similarity index 100%
rename from tests/lean/630.lean
rename to tests/lean_before_refactoring/630.lean
diff --git a/tests/lean/630.lean.expected.out b/tests/lean_before_refactoring/630.lean.expected.out
similarity index 100%
rename from tests/lean/630.lean.expected.out
rename to tests/lean_before_refactoring/630.lean.expected.out
diff --git a/tests/lean/768.lean b/tests/lean_before_refactoring/768.lean
similarity index 100%
rename from tests/lean/768.lean
rename to tests/lean_before_refactoring/768.lean
diff --git a/tests/lean/768.lean.expected.out b/tests/lean_before_refactoring/768.lean.expected.out
similarity index 100%
rename from tests/lean/768.lean.expected.out
rename to tests/lean_before_refactoring/768.lean.expected.out
diff --git a/tests/lean/793a.lean b/tests/lean_before_refactoring/793a.lean
similarity index 100%
rename from tests/lean/793a.lean
rename to tests/lean_before_refactoring/793a.lean
diff --git a/tests/lean/793a.lean.expected.out b/tests/lean_before_refactoring/793a.lean.expected.out
similarity index 100%
rename from tests/lean/793a.lean.expected.out
rename to tests/lean_before_refactoring/793a.lean.expected.out
diff --git a/tests/lean/793b.lean b/tests/lean_before_refactoring/793b.lean
similarity index 100%
rename from tests/lean/793b.lean
rename to tests/lean_before_refactoring/793b.lean
diff --git a/tests/lean/793b.lean.expected.out b/tests/lean_before_refactoring/793b.lean.expected.out
similarity index 100%
rename from tests/lean/793b.lean.expected.out
rename to tests/lean_before_refactoring/793b.lean.expected.out
diff --git a/tests/lean/800.lean b/tests/lean_before_refactoring/800.lean
similarity index 100%
rename from tests/lean/800.lean
rename to tests/lean_before_refactoring/800.lean
diff --git a/tests/lean/800.lean.expected.out b/tests/lean_before_refactoring/800.lean.expected.out
similarity index 100%
rename from tests/lean/800.lean.expected.out
rename to tests/lean_before_refactoring/800.lean.expected.out
diff --git a/tests/lean/axioms_of.lean b/tests/lean_before_refactoring/axioms_of.lean
similarity index 100%
rename from tests/lean/axioms_of.lean
rename to tests/lean_before_refactoring/axioms_of.lean
diff --git a/tests/lean/axioms_of.lean.expected.out b/tests/lean_before_refactoring/axioms_of.lean.expected.out
similarity index 100%
rename from tests/lean/axioms_of.lean.expected.out
rename to tests/lean_before_refactoring/axioms_of.lean.expected.out
diff --git a/tests/lean/binder_overload.lean b/tests/lean_before_refactoring/binder_overload.lean
similarity index 100%
rename from tests/lean/binder_overload.lean
rename to tests/lean_before_refactoring/binder_overload.lean
diff --git a/tests/lean/binder_overload.lean.expected.out b/tests/lean_before_refactoring/binder_overload.lean.expected.out
similarity index 100%
rename from tests/lean/binder_overload.lean.expected.out
rename to tests/lean_before_refactoring/binder_overload.lean.expected.out
diff --git a/tests/lean/coe2.lean b/tests/lean_before_refactoring/coe2.lean
similarity index 100%
rename from tests/lean/coe2.lean
rename to tests/lean_before_refactoring/coe2.lean
diff --git a/tests/lean/coe2.lean.expected.out b/tests/lean_before_refactoring/coe2.lean.expected.out
similarity index 100%
rename from tests/lean/coe2.lean.expected.out
rename to tests/lean_before_refactoring/coe2.lean.expected.out
diff --git a/tests/lean/eta_decls.lean b/tests/lean_before_refactoring/eta_decls.lean
similarity index 100%
rename from tests/lean/eta_decls.lean
rename to tests/lean_before_refactoring/eta_decls.lean
diff --git a/tests/lean/eta_decls.lean.expected.out b/tests/lean_before_refactoring/eta_decls.lean.expected.out
similarity index 100%
rename from tests/lean/eta_decls.lean.expected.out
rename to tests/lean_before_refactoring/eta_decls.lean.expected.out
diff --git a/tests/lean/finset_induction_bug.lean b/tests/lean_before_refactoring/finset_induction_bug.lean
similarity index 100%
rename from tests/lean/finset_induction_bug.lean
rename to tests/lean_before_refactoring/finset_induction_bug.lean
diff --git a/tests/lean/finset_induction_bug.lean.expected.out b/tests/lean_before_refactoring/finset_induction_bug.lean.expected.out
similarity index 100%
rename from tests/lean/finset_induction_bug.lean.expected.out
rename to tests/lean_before_refactoring/finset_induction_bug.lean.expected.out
diff --git a/tests/lean/gen_fail.lean b/tests/lean_before_refactoring/gen_fail.lean
similarity index 100%
rename from tests/lean/gen_fail.lean
rename to tests/lean_before_refactoring/gen_fail.lean
diff --git a/tests/lean/gen_fail.lean.expected.out b/tests/lean_before_refactoring/gen_fail.lean.expected.out
similarity index 100%
rename from tests/lean/gen_fail.lean.expected.out
rename to tests/lean_before_refactoring/gen_fail.lean.expected.out
diff --git a/tests/lean/list_vect_numerals.lean b/tests/lean_before_refactoring/list_vect_numerals.lean
similarity index 100%
rename from tests/lean/list_vect_numerals.lean
rename to tests/lean_before_refactoring/list_vect_numerals.lean
diff --git a/tests/lean/list_vect_numerals.lean.expected.out b/tests/lean_before_refactoring/list_vect_numerals.lean.expected.out
similarity index 100%
rename from tests/lean/list_vect_numerals.lean.expected.out
rename to tests/lean_before_refactoring/list_vect_numerals.lean.expected.out
diff --git a/tests/lean/nary_overload2.lean b/tests/lean_before_refactoring/nary_overload2.lean
similarity index 100%
rename from tests/lean/nary_overload2.lean
rename to tests/lean_before_refactoring/nary_overload2.lean
diff --git a/tests/lean/nary_overload2.lean.expected.out b/tests/lean_before_refactoring/nary_overload2.lean.expected.out
similarity index 100%
rename from tests/lean/nary_overload2.lean.expected.out
rename to tests/lean_before_refactoring/nary_overload2.lean.expected.out
diff --git a/tests/lean/noncomp_theory.lean b/tests/lean_before_refactoring/noncomp_theory.lean
similarity index 100%
rename from tests/lean/noncomp_theory.lean
rename to tests/lean_before_refactoring/noncomp_theory.lean
diff --git a/tests/lean/noncomp_theory.lean.expected.out b/tests/lean_before_refactoring/noncomp_theory.lean.expected.out
similarity index 100%
rename from tests/lean/noncomp_theory.lean.expected.out
rename to tests/lean_before_refactoring/noncomp_theory.lean.expected.out
diff --git a/tests/lean/nonexhaustive.lean b/tests/lean_before_refactoring/nonexhaustive.lean
similarity index 100%
rename from tests/lean/nonexhaustive.lean
rename to tests/lean_before_refactoring/nonexhaustive.lean
diff --git a/tests/lean/nonexhaustive.lean.expected.out b/tests/lean_before_refactoring/nonexhaustive.lean.expected.out
similarity index 100%
rename from tests/lean/nonexhaustive.lean.expected.out
rename to tests/lean_before_refactoring/nonexhaustive.lean.expected.out
diff --git a/tests/lean/norm1.lean b/tests/lean_before_refactoring/norm1.lean
similarity index 100%
rename from tests/lean/norm1.lean
rename to tests/lean_before_refactoring/norm1.lean
diff --git a/tests/lean/norm1.lean.expected.out b/tests/lean_before_refactoring/norm1.lean.expected.out
similarity index 100%
rename from tests/lean/norm1.lean.expected.out
rename to tests/lean_before_refactoring/norm1.lean.expected.out
diff --git a/tests/lean/notation_priority.lean b/tests/lean_before_refactoring/notation_priority.lean
similarity index 100%
rename from tests/lean/notation_priority.lean
rename to tests/lean_before_refactoring/notation_priority.lean
diff --git a/tests/lean/notation_priority.lean.expected.out b/tests/lean_before_refactoring/notation_priority.lean.expected.out
similarity index 100%
rename from tests/lean/notation_priority.lean.expected.out
rename to tests/lean_before_refactoring/notation_priority.lean.expected.out
diff --git a/tests/lean/rateval.lean b/tests/lean_before_refactoring/rateval.lean
similarity index 100%
rename from tests/lean/rateval.lean
rename to tests/lean_before_refactoring/rateval.lean
diff --git a/tests/lean/rateval.lean.expected.out b/tests/lean_before_refactoring/rateval.lean.expected.out
similarity index 100%
rename from tests/lean/rateval.lean.expected.out
rename to tests/lean_before_refactoring/rateval.lean.expected.out
diff --git a/tests/lean/revert_fail.lean b/tests/lean_before_refactoring/revert_fail.lean
similarity index 100%
rename from tests/lean/revert_fail.lean
rename to tests/lean_before_refactoring/revert_fail.lean
diff --git a/tests/lean/revert_fail.lean.expected.out b/tests/lean_before_refactoring/revert_fail.lean.expected.out
similarity index 100%
rename from tests/lean/revert_fail.lean.expected.out
rename to tests/lean_before_refactoring/revert_fail.lean.expected.out
diff --git a/tests/lean/run/505.lean b/tests/lean_before_refactoring/run/505.lean
similarity index 100%
rename from tests/lean/run/505.lean
rename to tests/lean_before_refactoring/run/505.lean
diff --git a/tests/lean/run/567.lean b/tests/lean_before_refactoring/run/567.lean
similarity index 100%
rename from tests/lean/run/567.lean
rename to tests/lean_before_refactoring/run/567.lean
diff --git a/tests/lean/run/585.lean b/tests/lean_before_refactoring/run/585.lean
similarity index 100%
rename from tests/lean/run/585.lean
rename to tests/lean_before_refactoring/run/585.lean
diff --git a/tests/lean/run/679a.lean b/tests/lean_before_refactoring/run/679a.lean
similarity index 100%
rename from tests/lean/run/679a.lean
rename to tests/lean_before_refactoring/run/679a.lean
diff --git a/tests/lean/run/679b.lean b/tests/lean_before_refactoring/run/679b.lean
similarity index 100%
rename from tests/lean/run/679b.lean
rename to tests/lean_before_refactoring/run/679b.lean
diff --git a/tests/lean/run/682.lean b/tests/lean_before_refactoring/run/682.lean
similarity index 100%
rename from tests/lean/run/682.lean
rename to tests/lean_before_refactoring/run/682.lean
diff --git a/tests/lean/run/687.lean b/tests/lean_before_refactoring/run/687.lean
similarity index 100%
rename from tests/lean/run/687.lean
rename to tests/lean_before_refactoring/run/687.lean
diff --git a/tests/lean/run/803.lean b/tests/lean_before_refactoring/run/803.lean
similarity index 100%
rename from tests/lean/run/803.lean
rename to tests/lean_before_refactoring/run/803.lean
diff --git a/tests/lean/run/809.lean b/tests/lean_before_refactoring/run/809.lean
similarity index 100%
rename from tests/lean/run/809.lean
rename to tests/lean_before_refactoring/run/809.lean
diff --git a/tests/lean/run/809b.lean b/tests/lean_before_refactoring/run/809b.lean
similarity index 100%
rename from tests/lean/run/809b.lean
rename to tests/lean_before_refactoring/run/809b.lean
diff --git a/tests/lean/run/abs.lean b/tests/lean_before_refactoring/run/abs.lean
similarity index 100%
rename from tests/lean/run/abs.lean
rename to tests/lean_before_refactoring/run/abs.lean
diff --git a/tests/lean/run/blast_cc8.lean b/tests/lean_before_refactoring/run/blast_cc8.lean
similarity index 100%
rename from tests/lean/run/blast_cc8.lean
rename to tests/lean_before_refactoring/run/blast_cc8.lean
diff --git a/tests/lean/run/blast_cc_subsingleton_normalization_issue.lean b/tests/lean_before_refactoring/run/blast_cc_subsingleton_normalization_issue.lean
similarity index 100%
rename from tests/lean/run/blast_cc_subsingleton_normalization_issue.lean
rename to tests/lean_before_refactoring/run/blast_cc_subsingleton_normalization_issue.lean
diff --git a/tests/lean/run/blast_ematch7.lean b/tests/lean_before_refactoring/run/blast_ematch7.lean
similarity index 100%
rename from tests/lean/run/blast_ematch7.lean
rename to tests/lean_before_refactoring/run/blast_ematch7.lean
diff --git a/tests/lean/run/blast_real_sub_issue.lean b/tests/lean_before_refactoring/run/blast_real_sub_issue.lean
similarity index 100%
rename from tests/lean/run/blast_real_sub_issue.lean
rename to tests/lean_before_refactoring/run/blast_real_sub_issue.lean
diff --git a/tests/lean/run/blast_safe_log_issue.lean b/tests/lean_before_refactoring/run/blast_safe_log_issue.lean
similarity index 100%
rename from tests/lean/run/blast_safe_log_issue.lean
rename to tests/lean_before_refactoring/run/blast_safe_log_issue.lean
diff --git a/tests/lean/run/blast_safe_log_issue2.lean b/tests/lean_before_refactoring/run/blast_safe_log_issue2.lean
similarity index 100%
rename from tests/lean/run/blast_safe_log_issue2.lean
rename to tests/lean_before_refactoring/run/blast_safe_log_issue2.lean
diff --git a/tests/lean/run/blast_tuple2.lean b/tests/lean_before_refactoring/run/blast_tuple2.lean
similarity index 100%
rename from tests/lean/run/blast_tuple2.lean
rename to tests/lean_before_refactoring/run/blast_tuple2.lean
diff --git a/tests/lean/run/choose_test.lean b/tests/lean_before_refactoring/run/choose_test.lean
similarity index 100%
rename from tests/lean/run/choose_test.lean
rename to tests/lean_before_refactoring/run/choose_test.lean
diff --git a/tests/lean/run/coe11.lean b/tests/lean_before_refactoring/run/coe11.lean
similarity index 100%
rename from tests/lean/run/coe11.lean
rename to tests/lean_before_refactoring/run/coe11.lean
diff --git a/tests/lean/run/coe_issue.lean b/tests/lean_before_refactoring/run/coe_issue.lean
similarity index 100%
rename from tests/lean/run/coe_issue.lean
rename to tests/lean_before_refactoring/run/coe_issue.lean
diff --git a/tests/lean/run/coe_issue2.lean b/tests/lean_before_refactoring/run/coe_issue2.lean
similarity index 100%
rename from tests/lean/run/coe_issue2.lean
rename to tests/lean_before_refactoring/run/coe_issue2.lean
diff --git a/tests/lean/run/coe_issue3.lean b/tests/lean_before_refactoring/run/coe_issue3.lean
similarity index 100%
rename from tests/lean/run/coe_issue3.lean
rename to tests/lean_before_refactoring/run/coe_issue3.lean
diff --git a/tests/lean/run/collision_bug.lean b/tests/lean_before_refactoring/run/collision_bug.lean
similarity index 100%
rename from tests/lean/run/collision_bug.lean
rename to tests/lean_before_refactoring/run/collision_bug.lean
diff --git a/tests/lean/run/congr.lean b/tests/lean_before_refactoring/run/congr.lean
similarity index 100%
rename from tests/lean/run/congr.lean
rename to tests/lean_before_refactoring/run/congr.lean
diff --git a/tests/lean/run/congr_tac2.lean b/tests/lean_before_refactoring/run/congr_tac2.lean
similarity index 100%
rename from tests/lean/run/congr_tac2.lean
rename to tests/lean_before_refactoring/run/congr_tac2.lean
diff --git a/tests/lean/run/deceq_vec.lean b/tests/lean_before_refactoring/run/deceq_vec.lean
similarity index 100%
rename from tests/lean/run/deceq_vec.lean
rename to tests/lean_before_refactoring/run/deceq_vec.lean
diff --git a/tests/lean/run/delta_issue1.lean b/tests/lean_before_refactoring/run/delta_issue1.lean
similarity index 100%
rename from tests/lean/run/delta_issue1.lean
rename to tests/lean_before_refactoring/run/delta_issue1.lean
diff --git a/tests/lean/run/dep_subst.lean b/tests/lean_before_refactoring/run/dep_subst.lean
similarity index 100%
rename from tests/lean/run/dep_subst.lean
rename to tests/lean_before_refactoring/run/dep_subst.lean
diff --git a/tests/lean/run/diag.lean b/tests/lean_before_refactoring/run/diag.lean
similarity index 100%
rename from tests/lean/run/diag.lean
rename to tests/lean_before_refactoring/run/diag.lean
diff --git a/tests/lean/run/eq18.lean b/tests/lean_before_refactoring/run/eq18.lean
similarity index 100%
rename from tests/lean/run/eq18.lean
rename to tests/lean_before_refactoring/run/eq18.lean
diff --git a/tests/lean/run/eq19.lean b/tests/lean_before_refactoring/run/eq19.lean
similarity index 100%
rename from tests/lean/run/eq19.lean
rename to tests/lean_before_refactoring/run/eq19.lean
diff --git a/tests/lean/run/eq3.lean b/tests/lean_before_refactoring/run/eq3.lean
similarity index 100%
rename from tests/lean/run/eq3.lean
rename to tests/lean_before_refactoring/run/eq3.lean
diff --git a/tests/lean/run/eq7.lean b/tests/lean_before_refactoring/run/eq7.lean
similarity index 100%
rename from tests/lean/run/eq7.lean
rename to tests/lean_before_refactoring/run/eq7.lean
diff --git a/tests/lean/run/eq8.lean b/tests/lean_before_refactoring/run/eq8.lean
similarity index 100%
rename from tests/lean/run/eq8.lean
rename to tests/lean_before_refactoring/run/eq8.lean
diff --git a/tests/lean/run/find_cmd.lean b/tests/lean_before_refactoring/run/find_cmd.lean
similarity index 100%
rename from tests/lean/run/find_cmd.lean
rename to tests/lean_before_refactoring/run/find_cmd.lean
diff --git a/tests/lean/run/finset_coe.lean b/tests/lean_before_refactoring/run/finset_coe.lean
similarity index 100%
rename from tests/lean/run/finset_coe.lean
rename to tests/lean_before_refactoring/run/finset_coe.lean
diff --git a/tests/lean/run/induction_tac1.lean b/tests/lean_before_refactoring/run/induction_tac1.lean
similarity index 100%
rename from tests/lean/run/induction_tac1.lean
rename to tests/lean_before_refactoring/run/induction_tac1.lean
diff --git a/tests/lean/run/inj_tac.lean b/tests/lean_before_refactoring/run/inj_tac.lean
similarity index 100%
rename from tests/lean/run/inj_tac.lean
rename to tests/lean_before_refactoring/run/inj_tac.lean
diff --git a/tests/lean/run/injective_decidable.lean b/tests/lean_before_refactoring/run/injective_decidable.lean
similarity index 100%
rename from tests/lean/run/injective_decidable.lean
rename to tests/lean_before_refactoring/run/injective_decidable.lean
diff --git a/tests/lean/run/inv_bug2.lean b/tests/lean_before_refactoring/run/inv_bug2.lean
similarity index 100%
rename from tests/lean/run/inv_bug2.lean
rename to tests/lean_before_refactoring/run/inv_bug2.lean
diff --git a/tests/lean/run/list_vector_overload.lean b/tests/lean_before_refactoring/run/list_vector_overload.lean
similarity index 100%
rename from tests/lean/run/list_vector_overload.lean
rename to tests/lean_before_refactoring/run/list_vector_overload.lean
diff --git a/tests/lean/run/local_ctx_bug.lean b/tests/lean_before_refactoring/run/local_ctx_bug.lean
similarity index 100%
rename from tests/lean/run/local_ctx_bug.lean
rename to tests/lean_before_refactoring/run/local_ctx_bug.lean
diff --git a/tests/lean/run/new_obtain3.lean b/tests/lean_before_refactoring/run/new_obtain3.lean
similarity index 100%
rename from tests/lean/run/new_obtain3.lean
rename to tests/lean_before_refactoring/run/new_obtain3.lean
diff --git a/tests/lean/run/new_obtain4.lean b/tests/lean_before_refactoring/run/new_obtain4.lean
similarity index 100%
rename from tests/lean/run/new_obtain4.lean
rename to tests/lean_before_refactoring/run/new_obtain4.lean
diff --git a/tests/lean/run/num_norm1.lean b/tests/lean_before_refactoring/run/num_norm1.lean
similarity index 100%
rename from tests/lean/run/num_norm1.lean
rename to tests/lean_before_refactoring/run/num_norm1.lean
diff --git a/tests/lean/run/override1.lean b/tests/lean_before_refactoring/run/override1.lean
similarity index 100%
rename from tests/lean/run/override1.lean
rename to tests/lean_before_refactoring/run/override1.lean
diff --git a/tests/lean/run/perm_with_pi_args.lean b/tests/lean_before_refactoring/run/perm_with_pi_args.lean
similarity index 100%
rename from tests/lean/run/perm_with_pi_args.lean
rename to tests/lean_before_refactoring/run/perm_with_pi_args.lean
diff --git a/tests/lean/run/pickle1.lean b/tests/lean_before_refactoring/run/pickle1.lean
similarity index 100%
rename from tests/lean/run/pickle1.lean
rename to tests/lean_before_refactoring/run/pickle1.lean
diff --git a/tests/lean/run/ppbeta.lean b/tests/lean_before_refactoring/run/ppbeta.lean
similarity index 100%
rename from tests/lean/run/ppbeta.lean
rename to tests/lean_before_refactoring/run/ppbeta.lean
diff --git a/tests/lean/run/print.lean b/tests/lean_before_refactoring/run/print.lean
similarity index 100%
rename from tests/lean/run/print.lean
rename to tests/lean_before_refactoring/run/print.lean
diff --git a/tests/lean/run/prio_overloading.lean b/tests/lean_before_refactoring/run/prio_overloading.lean
similarity index 100%
rename from tests/lean/run/prio_overloading.lean
rename to tests/lean_before_refactoring/run/prio_overloading.lean
diff --git a/tests/lean/run/rat_coe.lean b/tests/lean_before_refactoring/run/rat_coe.lean
similarity index 100%
rename from tests/lean/run/rat_coe.lean
rename to tests/lean_before_refactoring/run/rat_coe.lean
diff --git a/tests/lean/run/rat_rfl.lean b/tests/lean_before_refactoring/run/rat_rfl.lean
similarity index 100%
rename from tests/lean/run/rat_rfl.lean
rename to tests/lean_before_refactoring/run/rat_rfl.lean
diff --git a/tests/lean/run/refl_beta.lean b/tests/lean_before_refactoring/run/refl_beta.lean
similarity index 100%
rename from tests/lean/run/refl_beta.lean
rename to tests/lean_before_refactoring/run/refl_beta.lean
diff --git a/tests/lean/run/rewrite_with_beta.lean b/tests/lean_before_refactoring/run/rewrite_with_beta.lean
similarity index 100%
rename from tests/lean/run/rewrite_with_beta.lean
rename to tests/lean_before_refactoring/run/rewrite_with_beta.lean
diff --git a/tests/lean/run/rewriter6.lean b/tests/lean_before_refactoring/run/rewriter6.lean
similarity index 100%
rename from tests/lean/run/rewriter6.lean
rename to tests/lean_before_refactoring/run/rewriter6.lean
diff --git a/tests/lean/run/rewriter7.lean b/tests/lean_before_refactoring/run/rewriter7.lean
similarity index 100%
rename from tests/lean/run/rewriter7.lean
rename to tests/lean_before_refactoring/run/rewriter7.lean
diff --git a/tests/lean/run/string.lean b/tests/lean_before_refactoring/run/string.lean
similarity index 100%
rename from tests/lean/run/string.lean
rename to tests/lean_before_refactoring/run/string.lean
diff --git a/tests/lean/run/tactic16.lean b/tests/lean_before_refactoring/run/tactic16.lean
similarity index 100%
rename from tests/lean/run/tactic16.lean
rename to tests/lean_before_refactoring/run/tactic16.lean
diff --git a/tests/lean/run/tut_104.lean b/tests/lean_before_refactoring/run/tut_104.lean
similarity index 100%
rename from tests/lean/run/tut_104.lean
rename to tests/lean_before_refactoring/run/tut_104.lean
diff --git a/tests/lean/run/unfold_rec.lean b/tests/lean_before_refactoring/run/unfold_rec.lean
similarity index 100%
rename from tests/lean/run/unfold_rec.lean
rename to tests/lean_before_refactoring/run/unfold_rec.lean
diff --git a/tests/lean/run/unfold_rec2.lean b/tests/lean_before_refactoring/run/unfold_rec2.lean
similarity index 100%
rename from tests/lean/run/unfold_rec2.lean
rename to tests/lean_before_refactoring/run/unfold_rec2.lean
diff --git a/tests/lean/run/unfold_test.lean b/tests/lean_before_refactoring/run/unfold_test.lean
similarity index 100%
rename from tests/lean/run/unfold_test.lean
rename to tests/lean_before_refactoring/run/unfold_test.lean
diff --git a/tests/lean/run/univs.lean b/tests/lean_before_refactoring/run/univs.lean
similarity index 100%
rename from tests/lean/run/univs.lean
rename to tests/lean_before_refactoring/run/univs.lean
diff --git a/tests/lean/run/unzip_bug.lean b/tests/lean_before_refactoring/run/unzip_bug.lean
similarity index 100%
rename from tests/lean/run/unzip_bug.lean
rename to tests/lean_before_refactoring/run/unzip_bug.lean
diff --git a/tests/lean/run/user_recursor.lean b/tests/lean_before_refactoring/run/user_recursor.lean
similarity index 100%
rename from tests/lean/run/user_recursor.lean
rename to tests/lean_before_refactoring/run/user_recursor.lean
diff --git a/tests/lean/simplifier_light.lean b/tests/lean_before_refactoring/simplifier_light.lean
similarity index 100%
rename from tests/lean/simplifier_light.lean
rename to tests/lean_before_refactoring/simplifier_light.lean
diff --git a/tests/lean/simplifier_light.lean.expected.out b/tests/lean_before_refactoring/simplifier_light.lean.expected.out
similarity index 100%
rename from tests/lean/simplifier_light.lean.expected.out
rename to tests/lean_before_refactoring/simplifier_light.lean.expected.out
diff --git a/tests/lean/unfold_rec.lean b/tests/lean_before_refactoring/unfold_rec.lean
similarity index 100%
rename from tests/lean/unfold_rec.lean
rename to tests/lean_before_refactoring/unfold_rec.lean
diff --git a/tests/lean/unfold_rec.lean.expected.out b/tests/lean_before_refactoring/unfold_rec.lean.expected.out
similarity index 100%
rename from tests/lean/unfold_rec.lean.expected.out
rename to tests/lean_before_refactoring/unfold_rec.lean.expected.out
diff --git a/tests/lean/unzip_error.lean b/tests/lean_before_refactoring/unzip_error.lean
similarity index 100%
rename from tests/lean/unzip_error.lean
rename to tests/lean_before_refactoring/unzip_error.lean
diff --git a/tests/lean/unzip_error.lean.expected.out b/tests/lean_before_refactoring/unzip_error.lean.expected.out
similarity index 100%
rename from tests/lean/unzip_error.lean.expected.out
rename to tests/lean_before_refactoring/unzip_error.lean.expected.out
diff --git a/tests/lean/urec.lean b/tests/lean_before_refactoring/urec.lean
similarity index 100%
rename from tests/lean/urec.lean
rename to tests/lean_before_refactoring/urec.lean
diff --git a/tests/lean/urec.lean.expected.out b/tests/lean_before_refactoring/urec.lean.expected.out
similarity index 100%
rename from tests/lean/urec.lean.expected.out
rename to tests/lean_before_refactoring/urec.lean.expected.out