From 2da8e5afa1c5dd0fe3ce642723419db83d4c09f2 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Wed, 7 Apr 2021 22:29:19 -0700
Subject: [PATCH] chore: add completion test for the `group` issue

---
 tests/lean/interactive/completion5.lean              | 11 +++++++++++
 tests/lean/interactive/completion5.lean.expected.out |  8 ++++++++
 2 files changed, 19 insertions(+)
 create mode 100644 tests/lean/interactive/completion5.lean
 create mode 100644 tests/lean/interactive/completion5.lean.expected.out

diff --git a/tests/lean/interactive/completion5.lean b/tests/lean/interactive/completion5.lean
new file mode 100644
index 0000000000..5d9fffe661
--- /dev/null
+++ b/tests/lean/interactive/completion5.lean
@@ -0,0 +1,11 @@
+structure C where
+  f1 : Nat
+  f2 : Bool
+  b1 : String
+
+def f (c : C) : IO Unit :=
+  visit c
+where
+  visit (c : C) : IO Unit :=
+    let x := c.
+             --^ textDocument/completion
diff --git a/tests/lean/interactive/completion5.lean.expected.out b/tests/lean/interactive/completion5.lean.expected.out
new file mode 100644
index 0000000000..c3f14336b9
--- /dev/null
+++ b/tests/lean/interactive/completion5.lean.expected.out
@@ -0,0 +1,8 @@
+{"textDocument": {"uri": "file://completion5.lean"},
+ "position": {"line": 9, "character": 15}}
+{"items":
+ [{"label": "mk", "detail": "Nat → Bool → String → C"},
+  {"label": "b1", "detail": "C → String"},
+  {"label": "f1", "detail": "C → Nat"},
+  {"label": "f2", "detail": "C → Bool"}],
+ "isIncomplete": true}