@@ -86,8 +86,7 @@ pUsing :: SyntaxInfo -> IParser [PDecl]
8686pUsing syn =
8787 do reserved "using";
8888 lchar '('
89− ns <- sepBy1 (do x <- pfName; t <- pTSig syn; return (x,t))
90− (lchar ',')
89+ ns <- tyDeclList syn
9190 lchar ')'
9291 lchar '{'
9392 let uvars = using syn
@@ -153,19 +152,30 @@ pImplicitArg syn = do lchar '{'; n <- iName
153152pTSig syn = do lchar ':'
154153 pExpr syn
155154
156−pLambda syn = do lchar '\\'; x <- iName; t <- option Placeholder (pTSig syn)
155+pLambda syn = do lchar '\\';
156+ xt <- tyOptDeclList syn
157157 symbol "=>"
158158 sc <- pExpr syn
159− return (PLam x t sc)
159+ return (bindList PLam xt sc)
160160
161−pPi syn = do lchar '('; x <- iName; t <- pTSig syn; lchar ')'
161+pPi syn = do lchar '('; xt <- tyDeclList syn; lchar ')'
162162 symbol "->"
163163 sc <- pExpr syn
164− return (PPi Exp x t sc)
165− <|> do lchar '{'; x <- iName; t <- pTSig syn; lchar '}'
164+ return (bindList (PPi Exp) xt sc)
165+ <|> do lchar '{'; xt <- tyDeclList syn; lchar '}'
166166 symbol "->"
167167 sc <- pExpr syn
168− return (PPi Imp x t sc)
168+ return (bindList (PPi Imp) xt sc)
169+
170+tyDeclList syn = sepBy1 (do x <- pfName; t <- pTSig syn; return (x,t))
171+ (lchar ',')
172+
173+tyOptDeclList syn = sepBy1 (do x <- pfName; t <- option Placeholder (pTSig syn)
174+ return (x,t))
175+ (lchar ',')
176+
177+bindList b [] sc = sc
178+bindList b ((n, t):bs) sc = b n t (bindList b bs sc)
169179
170180table fixes
171181 = toTable (reverse fixes) ++