test: add class projection test

2020-01-09 16:24:53 -08:00 · 2020-01-09 16:24:53 -08:00 · 693d7dcf62
commit 693d7dcf62
parent a4c2b0303e
1 changed files with 15 additions and 0 deletions
--- a/tests/lean/run/new_frontend2.lean
+++ 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
+-/