From 0a0ca9f930edb89f18e562f14e2f6da1554edbbf Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Sun, 30 Aug 2020 08:10:58 -0700 Subject: [PATCH] fix: `funImplicitBinder` --- src/Lean/Parser/Term.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/Lean/Parser/Term.lean b/src/Lean/Parser/Term.lean index b9b119bf20..f3104e2db9 100644 --- a/src/Lean/Parser/Term.lean +++ b/src/Lean/Parser/Term.lean @@ -94,7 +94,7 @@ def bracketedBinder (requireType := false) := explicitBinder requireType <|> imp def simpleBinder := parser! many1 binderIdent @[builtinTermParser] def «forall» := parser!:leadPrec unicodeSymbol "∀ " "forall " >> many1 (simpleBinder <|> bracketedBinder) >> ", " >> termParser -def funImplicitBinder := try (lookahead ("{" >> many1 binderIdent >> " : ")) >> implicitBinder +def funImplicitBinder := try (lookahead ("{" >> many1 binderIdent >> (" : " <|> "}"))) >> implicitBinder def funBinder : Parser := funImplicitBinder <|> instBinder <|> termParser maxPrec @[builtinTermParser] def «fun» := parser!:maxPrec unicodeSymbol "λ " "fun " >> many1 funBinder >> darrow >> termParser