From 693d7dcf6221bee0b2e97b93559e707730c8acf7 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Thu, 9 Jan 2020 16:24:53 -0800
Subject: [PATCH] test: add class projection test

---
 tests/lean/run/new_frontend2.lean | 15 +++++++++++++++
 1 file changed, 15 insertions(+)
 create mode 100644 tests/lean/run/new_frontend2.lean

diff --git a/tests/lean/run/new_frontend2.lean b/tests/lean/run/new_frontend2.lean
new file mode 100644
index 0000000000..45ba4a9c74
--- /dev/null
+++ b/tests/lean/run/new_frontend2.lean
@@ -0,0 +1,15 @@
+new_frontend
+
+variable {m : Type → Type}
+variable [s : Functor m]
+
+#check s.map
+
+/-
+The following doesn't work because
+```
+variable [r : Monad m]
+#check r.map
+```
+because `Monad.to* methods have bad binder annotations
+-/