Allow underscore as a valid name for binder operator

src/Idris/Parser.idr

@@ -343,7 +343,8 @@ mutual
 
   opBinder : OriginDesc -> IndentInfo -> Rule (OperatorLHSInfo PTerm)
   opBinder fname indents
-      = do boundName <- bounds (UN . Basic <$> decoratedSimpleBinderName fname)
+      = do boundName <- bounds (UN <$> (Basic <$> decoratedSimpleBinderName fname
+                                       <|> symbol "_" $> Underscore))
            opBinderTypes fname indents boundName
 
   autobindOp : ParseOpts -> OriginDesc -> IndentInfo -> Rule PTerm

tests/idris2/operators/operators005/Test.idr

@@ -0,0 +1,19 @@
+
+import Data.String
+
+typebind infixr 0 :-
+autobind infixr 0 `for`
+
+record Container where
+  constructor (:-)
+  a1 : Type
+  a2 : a1 -> Type
+
+const : Type -> Type -> Container
+const a b = (_ : a) :- b
+
+test : Maybe (List Double)
+test = (_ := ["1", "two", "3"]) `for` Just 3
+
+test2 : Maybe (List Double)
+test2 = (_ : String := ["1", "two", "3"]) `for` Just 3

tests/idris2/operators/operators005/expected

@@ -0,0 +1 @@
+1/1: Building Test (Test.idr)

tests/idris2/operators/operators005/run

@@ -0,0 +1,3 @@
+. ../../../testutils.sh
+
+check Test.idr