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

@@ -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 :=

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