From b50597228b42a7eaa01bf8cb7a4fb1a98e7a8aab Mon Sep 17 00:00:00 2001 From: Gabriel Ebner Date: Sun, 6 Aug 2017 10:33:33 +0200 Subject: [PATCH] chore(tests/lean/print_ax2): remove duplicate and broken test --- tests/lean/print_ax2.lean | 1 - tests/lean/print_ax2.lean.expected.out | 2 -- 2 files changed, 3 deletions(-) delete mode 100644 tests/lean/print_ax2.lean delete mode 100644 tests/lean/print_ax2.lean.expected.out diff --git a/tests/lean/print_ax2.lean b/tests/lean/print_ax2.lean deleted file mode 100644 index efdcf5db5e..0000000000 --- a/tests/lean/print_ax2.lean +++ /dev/null @@ -1 +0,0 @@ -open subtype print axioms diff --git a/tests/lean/print_ax2.lean.expected.out b/tests/lean/print_ax2.lean.expected.out deleted file mode 100644 index 85a3793d7f..0000000000 --- a/tests/lean/print_ax2.lean.expected.out +++ /dev/null @@ -1,2 +0,0 @@ -print_ax2.lean:1:13: error: invalid namespace name 'print' -print_ax2.lean:1:25: error: invalid variables/constants/axioms declaration, ':' expected