sugar on lambdas
This commit is contained in:
@@ -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
|
||||
|
||||
|
||||
@@ -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
|
||||
|
||||
Reference in New Issue
Block a user