From d67546e388d7fc7d761bf3250cf7d9dd6bf59a5f Mon Sep 17 00:00:00 2001
From: Gabriel Ebner <gebner@gebner.org>
Date: Mon, 12 Sep 2022 15:44:16 +0200
Subject: [PATCH] chore: add test

---
 tests/lean/instance1.lean              | 9 +++++++++
 tests/lean/instance1.lean.expected.out | 1 +
 2 files changed, 10 insertions(+)
 create mode 100644 tests/lean/instance1.lean
 create mode 100644 tests/lean/instance1.lean.expected.out

diff --git a/tests/lean/instance1.lean b/tests/lean/instance1.lean
new file mode 100644
index 0000000000..9db054baa8
--- /dev/null
+++ b/tests/lean/instance1.lean
@@ -0,0 +1,9 @@
+def Mine := Id
+
+class MyMonad (m) extends Monad m where
+  bind_eq_bind : @bind = @bind := by trivial
+
+instance : MyMonad Mine where
+  -- should show me all the fields I need to fill in
+  -- excluding default and auto-param fields
+  -- i.e., only `pure` and `bind`
diff --git a/tests/lean/instance1.lean.expected.out b/tests/lean/instance1.lean.expected.out
new file mode 100644
index 0000000000..f09ccac7f6
--- /dev/null
+++ b/tests/lean/instance1.lean.expected.out
@@ -0,0 +1 @@
+instance1.lean:6:24-6:29: error: fields missing: 'pure', 'bind'