fix(tests/lean): move hott tests

2015-12-10 10:55:27 -08:00 · 2015-12-10 10:55:27 -08:00 · 13f9d8dd6c
commit 13f9d8dd6c
parent 7b29ee1666
2 changed files with 0 additions and 16 deletions
--- a/tests/lean/hott/876.hlean
+++ b/tests/lean/hott/876.hlean
--- a/tests/lean/run/415.hlean
+++ b/tests/lean/run/415.hlean
@ -1,16 +0,0 @@
-import algebra.group
-open path_algebra
-
-variable {A : Type}
-variable [s : add_comm_group A]
-include s
-
-theorem add_minus_cancel_left1 (a b c : A) : (c + a) - (c + b) = a - b :=
-begin
-  rotate_left 1,
-  apply sorry
-end
-
-theorem add_minus_cancel_left2 (a b c : A) : (c + a) - (c + b) = a - b :=
-by rotate_left 1;
-   apply sorry