From 4a43e33d45ac52095f01be7ed4f0ee7c0a847088 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Thu, 3 Mar 2016 13:43:08 -0800 Subject: [PATCH] chore(*): disable big chunk of the standard library and tests --- library/.project | 37 ++++++++++++++++++- library/data/default.lean | 8 ++-- library/data/list/comb.lean | 6 ++- library/data/nat/bigops.lean | 2 + library/data/nat/parity.lean | 2 + library/data/nat/power.lean | 4 ++ src/shell/CMakeLists.txt | 22 +++++------ src/tests/shell/file1.lean | 2 +- src/tests/shell/file2.lean | 2 +- tests/lean/interactive/coe.input | 3 -- tests/lean/interactive/coe.input.expected.out | 13 ------- tests/lean/interactive/coe.lean | 9 ----- tests/lean/run/coe10.lean | 17 --------- .../491.lean | 0 .../491.lean.expected.out | 0 .../583.lean | 0 .../583.lean.expected.out | 0 .../630.lean | 0 .../630.lean.expected.out | 0 .../768.lean | 0 .../768.lean.expected.out | 0 .../793a.lean | 0 .../793a.lean.expected.out | 0 .../793b.lean | 0 .../793b.lean.expected.out | 0 .../800.lean | 0 .../800.lean.expected.out | 0 .../axioms_of.lean | 0 .../axioms_of.lean.expected.out | 0 .../binder_overload.lean | 0 .../binder_overload.lean.expected.out | 0 .../coe2.lean | 0 .../coe2.lean.expected.out | 0 .../eta_decls.lean | 0 .../eta_decls.lean.expected.out | 0 .../finset_induction_bug.lean | 0 .../finset_induction_bug.lean.expected.out | 0 .../gen_fail.lean | 0 .../gen_fail.lean.expected.out | 0 .../list_vect_numerals.lean | 0 .../list_vect_numerals.lean.expected.out | 0 .../nary_overload2.lean | 0 .../nary_overload2.lean.expected.out | 0 .../noncomp_theory.lean | 0 .../noncomp_theory.lean.expected.out | 0 .../nonexhaustive.lean | 0 .../nonexhaustive.lean.expected.out | 0 .../norm1.lean | 0 .../norm1.lean.expected.out | 0 .../notation_priority.lean | 0 .../notation_priority.lean.expected.out | 0 .../rateval.lean | 0 .../rateval.lean.expected.out | 0 .../revert_fail.lean | 0 .../revert_fail.lean.expected.out | 0 .../run/505.lean | 0 .../run/567.lean | 0 .../run/585.lean | 0 .../run/679a.lean | 0 .../run/679b.lean | 0 .../run/682.lean | 0 .../run/687.lean | 0 .../run/803.lean | 0 .../run/809.lean | 0 .../run/809b.lean | 0 .../run/abs.lean | 0 .../run/blast_cc8.lean | 0 ...t_cc_subsingleton_normalization_issue.lean | 0 .../run/blast_ematch7.lean | 0 .../run/blast_real_sub_issue.lean | 0 .../run/blast_safe_log_issue.lean | 0 .../run/blast_safe_log_issue2.lean | 0 .../run/blast_tuple2.lean | 0 .../run/choose_test.lean | 0 .../run/coe11.lean | 0 .../run/coe_issue.lean | 0 .../run/coe_issue2.lean | 0 .../run/coe_issue3.lean | 0 .../run/collision_bug.lean | 0 .../run/congr.lean | 0 .../run/congr_tac2.lean | 0 .../run/deceq_vec.lean | 0 .../run/delta_issue1.lean | 0 .../run/dep_subst.lean | 0 .../run/diag.lean | 0 .../run/eq18.lean | 0 .../run/eq19.lean | 0 .../run/eq3.lean | 0 .../run/eq7.lean | 0 .../run/eq8.lean | 0 .../run/find_cmd.lean | 0 .../run/finset_coe.lean | 0 .../run/induction_tac1.lean | 0 .../run/inj_tac.lean | 0 .../run/injective_decidable.lean | 0 .../run/inv_bug2.lean | 0 .../run/list_vector_overload.lean | 0 .../run/local_ctx_bug.lean | 0 .../run/new_obtain3.lean | 0 .../run/new_obtain4.lean | 0 .../run/num_norm1.lean | 0 .../run/override1.lean | 0 .../run/perm_with_pi_args.lean | 0 .../run/pickle1.lean | 0 .../run/ppbeta.lean | 0 .../run/print.lean | 0 .../run/prio_overloading.lean | 0 .../run/rat_coe.lean | 0 .../run/rat_rfl.lean | 0 .../run/refl_beta.lean | 0 .../run/rewrite_with_beta.lean | 0 .../run/rewriter6.lean | 0 .../run/rewriter7.lean | 0 .../run/string.lean | 0 .../run/tactic16.lean | 0 .../run/tut_104.lean | 0 .../run/unfold_rec.lean | 0 .../run/unfold_rec2.lean | 0 .../run/unfold_test.lean | 0 .../run/univs.lean | 0 .../run/unzip_bug.lean | 0 .../run/user_recursor.lean | 0 .../simplifier_light.lean | 0 .../simplifier_light.lean.expected.out | 0 .../unfold_rec.lean | 0 .../unfold_rec.lean.expected.out | 0 .../unzip_error.lean | 0 .../unzip_error.lean.expected.out | 0 .../urec.lean | 0 .../urec.lean.expected.out | 0 130 files changed, 67 insertions(+), 60 deletions(-) delete mode 100644 tests/lean/interactive/coe.input delete mode 100644 tests/lean/interactive/coe.input.expected.out delete mode 100644 tests/lean/interactive/coe.lean delete mode 100644 tests/lean/run/coe10.lean rename tests/{lean => lean_before_refactoring}/491.lean (100%) rename tests/{lean => lean_before_refactoring}/491.lean.expected.out (100%) rename tests/{lean => lean_before_refactoring}/583.lean (100%) rename tests/{lean => lean_before_refactoring}/583.lean.expected.out (100%) rename tests/{lean => lean_before_refactoring}/630.lean (100%) rename tests/{lean => lean_before_refactoring}/630.lean.expected.out (100%) rename tests/{lean => lean_before_refactoring}/768.lean (100%) rename tests/{lean => lean_before_refactoring}/768.lean.expected.out (100%) rename tests/{lean => lean_before_refactoring}/793a.lean (100%) rename tests/{lean => lean_before_refactoring}/793a.lean.expected.out (100%) rename tests/{lean => lean_before_refactoring}/793b.lean (100%) rename tests/{lean => lean_before_refactoring}/793b.lean.expected.out (100%) rename tests/{lean => lean_before_refactoring}/800.lean (100%) rename tests/{lean => lean_before_refactoring}/800.lean.expected.out (100%) rename tests/{lean => lean_before_refactoring}/axioms_of.lean (100%) rename tests/{lean => lean_before_refactoring}/axioms_of.lean.expected.out (100%) rename tests/{lean => lean_before_refactoring}/binder_overload.lean (100%) rename tests/{lean => lean_before_refactoring}/binder_overload.lean.expected.out (100%) rename tests/{lean => lean_before_refactoring}/coe2.lean (100%) rename tests/{lean => lean_before_refactoring}/coe2.lean.expected.out (100%) rename tests/{lean => lean_before_refactoring}/eta_decls.lean (100%) rename tests/{lean => lean_before_refactoring}/eta_decls.lean.expected.out (100%) rename tests/{lean => lean_before_refactoring}/finset_induction_bug.lean (100%) rename tests/{lean => lean_before_refactoring}/finset_induction_bug.lean.expected.out (100%) rename tests/{lean => lean_before_refactoring}/gen_fail.lean (100%) rename tests/{lean => lean_before_refactoring}/gen_fail.lean.expected.out (100%) rename tests/{lean => lean_before_refactoring}/list_vect_numerals.lean (100%) rename tests/{lean => lean_before_refactoring}/list_vect_numerals.lean.expected.out (100%) rename tests/{lean => lean_before_refactoring}/nary_overload2.lean (100%) rename tests/{lean => lean_before_refactoring}/nary_overload2.lean.expected.out (100%) rename tests/{lean => lean_before_refactoring}/noncomp_theory.lean (100%) rename tests/{lean => lean_before_refactoring}/noncomp_theory.lean.expected.out (100%) rename tests/{lean => lean_before_refactoring}/nonexhaustive.lean (100%) rename tests/{lean => lean_before_refactoring}/nonexhaustive.lean.expected.out (100%) rename tests/{lean => lean_before_refactoring}/norm1.lean (100%) rename tests/{lean => lean_before_refactoring}/norm1.lean.expected.out (100%) rename tests/{lean => lean_before_refactoring}/notation_priority.lean (100%) rename tests/{lean => lean_before_refactoring}/notation_priority.lean.expected.out (100%) rename tests/{lean => lean_before_refactoring}/rateval.lean (100%) rename tests/{lean => lean_before_refactoring}/rateval.lean.expected.out (100%) rename tests/{lean => lean_before_refactoring}/revert_fail.lean (100%) rename tests/{lean => lean_before_refactoring}/revert_fail.lean.expected.out (100%) rename tests/{lean => lean_before_refactoring}/run/505.lean (100%) rename tests/{lean => lean_before_refactoring}/run/567.lean (100%) rename tests/{lean => lean_before_refactoring}/run/585.lean (100%) rename tests/{lean => lean_before_refactoring}/run/679a.lean (100%) rename tests/{lean => lean_before_refactoring}/run/679b.lean (100%) rename tests/{lean => lean_before_refactoring}/run/682.lean (100%) rename tests/{lean => lean_before_refactoring}/run/687.lean (100%) rename tests/{lean => lean_before_refactoring}/run/803.lean (100%) rename tests/{lean => lean_before_refactoring}/run/809.lean (100%) rename tests/{lean => lean_before_refactoring}/run/809b.lean (100%) rename tests/{lean => lean_before_refactoring}/run/abs.lean (100%) rename tests/{lean => lean_before_refactoring}/run/blast_cc8.lean (100%) rename tests/{lean => lean_before_refactoring}/run/blast_cc_subsingleton_normalization_issue.lean (100%) rename tests/{lean => lean_before_refactoring}/run/blast_ematch7.lean (100%) rename tests/{lean => lean_before_refactoring}/run/blast_real_sub_issue.lean (100%) rename tests/{lean => lean_before_refactoring}/run/blast_safe_log_issue.lean (100%) rename tests/{lean => lean_before_refactoring}/run/blast_safe_log_issue2.lean (100%) rename tests/{lean => lean_before_refactoring}/run/blast_tuple2.lean (100%) rename tests/{lean => lean_before_refactoring}/run/choose_test.lean (100%) rename tests/{lean => lean_before_refactoring}/run/coe11.lean (100%) rename tests/{lean => lean_before_refactoring}/run/coe_issue.lean (100%) rename tests/{lean => lean_before_refactoring}/run/coe_issue2.lean (100%) rename tests/{lean => lean_before_refactoring}/run/coe_issue3.lean (100%) rename tests/{lean => lean_before_refactoring}/run/collision_bug.lean (100%) rename tests/{lean => lean_before_refactoring}/run/congr.lean (100%) rename tests/{lean => lean_before_refactoring}/run/congr_tac2.lean (100%) rename tests/{lean => lean_before_refactoring}/run/deceq_vec.lean (100%) rename tests/{lean => lean_before_refactoring}/run/delta_issue1.lean (100%) rename tests/{lean => lean_before_refactoring}/run/dep_subst.lean (100%) rename tests/{lean => lean_before_refactoring}/run/diag.lean (100%) rename tests/{lean => lean_before_refactoring}/run/eq18.lean (100%) rename tests/{lean => lean_before_refactoring}/run/eq19.lean (100%) rename tests/{lean => lean_before_refactoring}/run/eq3.lean (100%) rename tests/{lean => lean_before_refactoring}/run/eq7.lean (100%) rename tests/{lean => lean_before_refactoring}/run/eq8.lean (100%) rename tests/{lean => lean_before_refactoring}/run/find_cmd.lean (100%) rename tests/{lean => lean_before_refactoring}/run/finset_coe.lean (100%) rename tests/{lean => lean_before_refactoring}/run/induction_tac1.lean (100%) rename tests/{lean => lean_before_refactoring}/run/inj_tac.lean (100%) rename tests/{lean => lean_before_refactoring}/run/injective_decidable.lean (100%) rename tests/{lean => lean_before_refactoring}/run/inv_bug2.lean (100%) rename tests/{lean => lean_before_refactoring}/run/list_vector_overload.lean (100%) rename tests/{lean => lean_before_refactoring}/run/local_ctx_bug.lean (100%) rename tests/{lean => lean_before_refactoring}/run/new_obtain3.lean (100%) rename tests/{lean => lean_before_refactoring}/run/new_obtain4.lean (100%) rename tests/{lean => lean_before_refactoring}/run/num_norm1.lean (100%) rename tests/{lean => lean_before_refactoring}/run/override1.lean (100%) rename tests/{lean => lean_before_refactoring}/run/perm_with_pi_args.lean (100%) rename tests/{lean => lean_before_refactoring}/run/pickle1.lean (100%) rename tests/{lean => lean_before_refactoring}/run/ppbeta.lean (100%) rename tests/{lean => lean_before_refactoring}/run/print.lean (100%) rename tests/{lean => lean_before_refactoring}/run/prio_overloading.lean (100%) rename tests/{lean => lean_before_refactoring}/run/rat_coe.lean (100%) rename tests/{lean => lean_before_refactoring}/run/rat_rfl.lean (100%) rename tests/{lean => lean_before_refactoring}/run/refl_beta.lean (100%) rename tests/{lean => lean_before_refactoring}/run/rewrite_with_beta.lean (100%) rename tests/{lean => lean_before_refactoring}/run/rewriter6.lean (100%) rename tests/{lean => lean_before_refactoring}/run/rewriter7.lean (100%) rename tests/{lean => lean_before_refactoring}/run/string.lean (100%) rename tests/{lean => lean_before_refactoring}/run/tactic16.lean (100%) rename tests/{lean => lean_before_refactoring}/run/tut_104.lean (100%) rename tests/{lean => lean_before_refactoring}/run/unfold_rec.lean (100%) rename tests/{lean => lean_before_refactoring}/run/unfold_rec2.lean (100%) rename tests/{lean => lean_before_refactoring}/run/unfold_test.lean (100%) rename tests/{lean => lean_before_refactoring}/run/univs.lean (100%) rename tests/{lean => lean_before_refactoring}/run/unzip_bug.lean (100%) rename tests/{lean => lean_before_refactoring}/run/user_recursor.lean (100%) rename tests/{lean => lean_before_refactoring}/simplifier_light.lean (100%) rename tests/{lean => lean_before_refactoring}/simplifier_light.lean.expected.out (100%) rename tests/{lean => lean_before_refactoring}/unfold_rec.lean (100%) rename tests/{lean => lean_before_refactoring}/unfold_rec.lean.expected.out (100%) rename tests/{lean => lean_before_refactoring}/unzip_error.lean (100%) rename tests/{lean => lean_before_refactoring}/unzip_error.lean.expected.out (100%) rename tests/{lean => lean_before_refactoring}/urec.lean (100%) rename tests/{lean => lean_before_refactoring}/urec.lean.expected.out (100%) 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