From 825d9643cd33bca74f774ebd57e27bef2ea5a379 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Sun, 30 Aug 2020 07:35:41 -0700
Subject: [PATCH] feat: allow structure instances as `fun` binder without `()`

The issue is that `{ x := ... }` was being parsed as an implicit
binder, and we were getting an error at `:=`.
---
 src/Lean/Parser/Term.lean | 3 ++-
 tests/lean/match1.lean    | 9 +++++++++
 2 files changed, 11 insertions(+), 1 deletion(-)

diff --git a/src/Lean/Parser/Term.lean b/src/Lean/Parser/Term.lean
index 3ad222a4d5..b3ee679ea3 100644
--- a/src/Lean/Parser/Term.lean
+++ b/src/Lean/Parser/Term.lean
@@ -92,7 +92,8 @@ def bracketedBinder (requireType := false) := explicitBinder requireType <|> imp
 def simpleBinder := parser! many1 binderIdent
 @[builtinTermParser] def «forall» := parser!:leadPrec unicodeSymbol "∀ " "forall " >> many1 (simpleBinder <|> bracketedBinder) >> ", " >> termParser
 
-def funBinder : Parser := implicitBinder <|> instBinder <|> termParser maxPrec
+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
 
 def matchAlt : Parser :=
diff --git a/tests/lean/match1.lean b/tests/lean/match1.lean
index ee8e7f0f26..b17676186d 100644
--- a/tests/lean/match1.lean
+++ b/tests/lean/match1.lean
@@ -55,3 +55,12 @@ match h with
 def f (x : Nat × Nat) : Bool × Bool × Bool → Nat :=
 match x with
 | (a, b) => fun _ => a
+
+structure S :=
+(x y z : Nat := 0)
+
+def f1 : S → S :=
+fun { x := x, ..} => { y := x }
+
+theorem ex2 : f1 { x := 10 } = { y := 10 } :=
+rfl