doc: elabissue for underapplied proj notation

tests/elabissues/ProjNotation.lean

@@ -0,0 +1,11 @@
+/- Underapplying a projection notation applies the 'this' argument to the wrong parameter.
+   It should either fail or (preferably) construct an explicit lambda. -/
+
+-- Char → Bool
+#check fun c => ['a', 'b'].elem c
+-- List (List Char) → Bool
+#check ['a', 'b'].elem
+-- works
+#check fun (s : String) => s.split (fun c => ['a', 'b'].elem c)
+-- doesn't work
+#check fun (s : String) => s.split (['a', 'b'].elem)