diff --git a/eg/ex.newt b/eg/ex.newt index 9d15bba..fe3f03e 100644 --- a/eg/ex.newt +++ b/eg/ex.newt @@ -11,9 +11,8 @@ id = \ a => \ x => x List : U -> U List = \ A => (L : U) -> L -> (A -> L -> L) -> L --- need more sugar for lambdas nil : (A L : U) -> L -> (A -> L -> L) -> L -nil = \ A => \ L => \ n => \ f => n +nil = \ A L n f => n Bool : U diff --git a/src/Lib/Parser.idr b/src/Lib/Parser.idr index 1bd7735..5f43086 100644 --- a/src/Lib/Parser.idr +++ b/src/Lib/Parser.idr @@ -141,11 +141,10 @@ lamExpr : Parser Raw lamExpr = do keyword "\\" commit - (icit, name, ty) <- pLetArg + args <- some pLetArg keyword "=>" scope <- typeExpr - -- TODO optional type - pure $ RLam name icit scope + pure $ foldr (\(icit, name, ty), sc => RLam name icit sc) scope args pPattern : Parser Pattern pPattern