From ea9a9d63d145ab368b44970fb2e66ac90fe56c3b Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Fri, 30 Jan 2015 09:49:34 -0800
Subject: [PATCH] test(tests/lean): add tests for structure command error
 messages

---
 tests/lean/bad_structures2.lean              | 31 ++++++++++++++++++++
 tests/lean/bad_structures2.lean.expected.out | 11 +++++++
 2 files changed, 42 insertions(+)
 create mode 100644 tests/lean/bad_structures2.lean
 create mode 100644 tests/lean/bad_structures2.lean.expected.out

diff --git a/tests/lean/bad_structures2.lean b/tests/lean/bad_structures2.lean
new file mode 100644
index 0000000000..b9c0a20c95
--- /dev/null
+++ b/tests/lean/bad_structures2.lean
@@ -0,0 +1,31 @@
+structure foo :=
+(x : bool)
+
+structure boo :=
+(x : nat)
+
+structure bla extends foo, boo
+
+structure boo2 :=
+{x : bool}
+
+structure bla extends foo, boo2
+
+structure bla extends foo :=
+(x : num)
+
+structure bla extends foo :=
+( : num)
+
+structure bla extends foo :=
+mk :: y z : num
+
+structure bla2 extends foo renaming y → z
+
+structure bla2 extends nat
+
+structure bla2 extends Type
+
+
+structure bla2 : Prop :=
+(x : Prop)
diff --git a/tests/lean/bad_structures2.lean.expected.out b/tests/lean/bad_structures2.lean.expected.out
new file mode 100644
index 0000000000..653deefb39
--- /dev/null
+++ b/tests/lean/bad_structures2.lean.expected.out
@@ -0,0 +1,11 @@
+bad_structures2.lean:7:27: error: invalid 'structure' header, field 'x' from 'boo' has already been declared with a different type
+  bool
+and
+  nat
+bad_structures2.lean:12:27: error: invalid 'structure' header, field 'x' has already been declared with a different binder annotation
+bad_structures2.lean:15:1: error: field 'x' has been declared in parent structure
+bad_structures2.lean:18:2: error: invalid field, identifier expected
+bad_structures2.lean:23:36: error: invalid 'structure' renaming, parent structure 'foo' does not contain field 'y'
+bad_structures2.lean:25:23: error: invalid 'structure' extends, 'nat' is not a structure
+bad_structures2.lean:27:23: error: invalid 'structure', expression must be a 'parent' structure
+bad_structures2.lean:30:15: error: invalid 'structure', 'Type' expected