From 16392fda7d99fd40a4cac3317a4a0da40fe287da Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Wed, 15 Mar 2017 20:37:53 -0700 Subject: [PATCH] chore(tests/lean/inductive_sorry): remove test --- tests/lean/inductive_sorry.lean | 12 ------------ tests/lean/inductive_sorry.lean.expected.out | 5 ----- 2 files changed, 17 deletions(-) delete mode 100644 tests/lean/inductive_sorry.lean delete mode 100644 tests/lean/inductive_sorry.lean.expected.out diff --git a/tests/lean/inductive_sorry.lean b/tests/lean/inductive_sorry.lean deleted file mode 100644 index 1c6cdc314c..0000000000 --- a/tests/lean/inductive_sorry.lean +++ /dev/null @@ -1,12 +0,0 @@ -inductive foo (A : sorry → ℕ) -| mk : foo - -inductive foo : sorry → ℕ -| mk : foo 0 - -inductive foo -| mk : sorry → foo - -structure foo (A : sorry → ℕ) := (x : ℕ) - -structure foo : Type := (x : bool → sorry) diff --git a/tests/lean/inductive_sorry.lean.expected.out b/tests/lean/inductive_sorry.lean.expected.out deleted file mode 100644 index 9e23205657..0000000000 --- a/tests/lean/inductive_sorry.lean.expected.out +++ /dev/null @@ -1,5 +0,0 @@ -inductive_sorry.lean:1:0: error: type of parameter 'A' contains 'sorry' -inductive_sorry.lean:4:0: error: type of parameter 'foo' contains 'sorry' -inductive_sorry.lean:7:0: error: constructor 'foo.mk' contains 'sorry' -inductive_sorry.lean:10:0: error: type of parameter 'A' contains 'sorry' -inductive_sorry.lean:12:0: error: field 'x' contains 'sorry'