From d2910337af1ff6d731b7dd63ea52de74a3e6f33f Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Mon, 12 Apr 2021 22:32:27 -0700
Subject: [PATCH] test: completion

---
 tests/lean/interactive/completion7.lean            |  4 ++++
 .../lean/interactive/completion7.lean.expected.out | 14 ++++++++++++++
 2 files changed, 18 insertions(+)
 create mode 100644 tests/lean/interactive/completion7.lean
 create mode 100644 tests/lean/interactive/completion7.lean.expected.out

diff --git a/tests/lean/interactive/completion7.lean b/tests/lean/interactive/completion7.lean
new file mode 100644
index 0000000000..2c2abc6a51
--- /dev/null
+++ b/tests/lean/interactive/completion7.lean
@@ -0,0 +1,4 @@
+#check And
+        --^ textDocument/completion
+#check And.
+         --^ textDocument/completion
diff --git a/tests/lean/interactive/completion7.lean.expected.out b/tests/lean/interactive/completion7.lean.expected.out
new file mode 100644
index 0000000000..9becc008bb
--- /dev/null
+++ b/tests/lean/interactive/completion7.lean.expected.out
@@ -0,0 +1,14 @@
+{"textDocument": {"uri": "file://completion7.lean"},
+ "position": {"line": 0, "character": 10}}
+{"items":
+ [{"label": "And", "detail": "Prop → Prop → Prop"},
+  {"label": "AndOp", "detail": "Type u → Type u"},
+  {"label": "AndThen", "detail": "Type u → Type u"}],
+ "isIncomplete": true}
+{"textDocument": {"uri": "file://completion7.lean"},
+ "position": {"line": 2, "character": 11}}
+{"items":
+ [{"label": "intro", "detail": "?a → ?b → ?a ∧ ?b"},
+  {"label": "left", "detail": "?a ∧ ?b → ?a"},
+  {"label": "right", "detail": "?a ∧ ?b → ?b"}],
+ "isIncomplete": true}