sugar on binders

eg/ex.newt

@@ -12,7 +12,7 @@ List : U -> U
 List = \ A => (L : U) -> L -> (A -> L -> L) -> L
 
 -- need more sugar for lambdas
-nil : (A : U) -> (L : U) -> L -> (A -> L -> L) -> L
+nil : (A L : U) -> L -> (A -> L -> L) -> L
 nil = \ A => \ L => \ n => \ f => n
 
 Bool : U

src/Lib/Parser.idr

@@ -176,36 +176,37 @@ term =  caseExpr
     <|> lamExpr
     <|> parseOp
 
-expBinder : Parser Raw
+
-expBinder = do
+ebind : Parser (List (String, Icit, Raw))
+ebind = do
   sym "("
-  name <- ident
+  names <- some ident
   sym ":"
   ty <- typeExpr
   sym ")"
-  sym "->"
+  pure $ map (\name => (name, Explicit, ty)) names
-  scope <- typeExpr
-  pure $ RPi (Just name) Explicit ty scope
 
-impBinder : Parser Raw
+ibind : Parser (List (String, Icit, Raw))
-impBinder = do
+ibind = do
   sym "{"
-  name <- ident
+  names <- some ident
   sym ":"
   ty <- typeExpr
   sym "}"
+  pure $ map (\name => (name, Explicit, ty)) names
+
+-- Collect a bunch of binders (A : U) {y : A} -> ...
+binders : Parser Raw
+binders = do  
+  binds <- many (ibind <|> ebind)
   sym "->"
   scope <- typeExpr
-  pure $ RPi (Just name) Implicit ty scope
+  pure $ foldr mkBind scope (join binds)
+  where
+    mkBind : (String, Icit, Raw) -> Raw -> Raw
+    mkBind (name, icit, ty) scope = RPi (Just name) icit ty scope
 
--- something binder looking
+typeExpr = binders
--- todo sepby space or whatever
-export
-binder : Parser Raw
-binder = expBinder <|> impBinder
-
-
-typeExpr = binder
   <|> do
         exp <- term
         scope <- optional (sym "->" *> mustWork typeExpr)