From 511bf69dd4b55f0fc6d4cc66937bbfa6d91ecfcb Mon Sep 17 00:00:00 2001
From: Sebastian Ullrich <sebasti@nullri.ch>
Date: Wed, 22 Nov 2017 18:25:30 +0100
Subject: [PATCH] chore(tests): forgot to commit structure instance test

---
 tests/lean/structure_instances.lean           | 28 +++++++++++++++++++
 .../structure_instances.lean.expected.out     | 22 +++++++++++++++
 2 files changed, 50 insertions(+)
 create mode 100644 tests/lean/structure_instances.lean
 create mode 100644 tests/lean/structure_instances.lean.expected.out

diff --git a/tests/lean/structure_instances.lean b/tests/lean/structure_instances.lean
new file mode 100644
index 0000000000..4641df4b9b
--- /dev/null
+++ b/tests/lean/structure_instances.lean
@@ -0,0 +1,28 @@
+meta def mk_c := `[exact 1]
+
+structure foo (α : Type) :=
+(a : α)
+(b : α := a)
+(c : α . mk_c)
+
+def f : foo ℕ := {a := 1}
+#check ({a := 1} : foo ℕ)
+#check ({foo . a := 1} : foo ℕ)
+#check ({..} : foo ℕ)
+#check ({foo . ..} : foo ℕ)
+#check {c := 1, ..f}
+#check {..f}
+
+#check {.., a := 1} -- ".." must be last item
+#check {..f, a := 1} -- "..f" cannot be followed by key-value pair
+
+structure bar :=
+(a : ℕ := 0)
+(b : ℕ := 0)
+
+structure baz :=
+(b : ℕ := 2)
+(c : ℕ := 2)
+
+#check ({.} : bar)
+#check ({a := 1, ..{bar.}, ..{baz.}} : foo ℕ)
diff --git a/tests/lean/structure_instances.lean.expected.out b/tests/lean/structure_instances.lean.expected.out
new file mode 100644
index 0000000000..da07cf23d4
--- /dev/null
+++ b/tests/lean/structure_instances.lean.expected.out
@@ -0,0 +1,22 @@
+{a := 1, b := 1, c := 1} : foo ℕ
+{a := 1, b := 1, c := 1} : foo ℕ
+{a := ?M_1, b := ?M_1, c := 1} : foo ℕ
+{a := ?M_1, b := ?M_1, c := 1} : foo ℕ
+{a := f.a, b := f.b, c := 1} : foo ℕ
+{a := f.a, b := f.b, c := f.c} : foo ℕ
+structure_instances.lean:16:10: error: invalid expression
+structure_instances.lean:16:12: error: invalid structure instance, '}' expected
+structure_instances.lean:16:7: error: invalid structure notation source, not a structure
+  ⁇
+which has type
+  ?m_1
+structure_instances.lean:16:7: error: invalid structure value {...}, expected type is not known(solution: use qualified structure instance { struct_id . ... }
+structure_instances.lean:16:14: error: command expected
+structure_instances.lean:17:13: error: invalid structure instance, '}' expected
+structure_instances.lean:17:7: error: function expected at
+  {a := f.a, b := f.b, c := f.c}
+term has type
+  foo ℕ
+structure_instances.lean:17:15: error: command expected
+{a := 0, b := 0} : bar
+{a := 1, b := {a := 0, b := 0}.b, c := {b := 2, c := 2}.c} : foo ℕ