feat: fun+match macro

Example:
```
fun
  | 0 => true
  | _ => false
```

src/Lean/Elab/Binders.lean

@@ -359,20 +359,6 @@ else do
   resettingSynthInstanceCacheWhen (s.localInsts.size > localInsts.size) $ withLCtx s.lctx s.localInsts $
     x s.fvars s.expectedType?
 
-@[builtinTermElab «fun»] def elabFun : TermElab :=
-fun stx expectedType? => do
--- `fun` term+ `=>` term
-let binders := (stx.getArg 1).getArgs;
-let body := stx.getArg 3;
-(binders, body, expandedPattern) ← expandFunBinders binders body;
-if expandedPattern then do
-  newStx ← `(fun $binders* => $body);
-  withMacroExpansion stx newStx $ elabTerm newStx expectedType?
-else
-  elabFunBinders binders expectedType? $ fun xs expectedType? => do
-    e ← elabTerm body expectedType?;
-    mkLambdaFVars xs e
-
 /-
   Recall that
   ```
@@ -420,6 +406,25 @@ private def expandMatchAltsIntoMatchAux (ref : Syntax) (matchAlts : Syntax) : Na
 def expandMatchAltsIntoMatch (ref : Syntax) (matchAlts : Syntax) : MacroM Syntax :=
 expandMatchAltsIntoMatchAux ref matchAlts (getMatchAltNumPatterns matchAlts) #[]
 
+@[builtinTermElab «fun»] def elabFun : TermElab :=
+fun stx expectedType? =>
+-- "fun " >> ((many1 funBinder >> darrow >> termParser) <|> funMatchAlts)
+-- funMatchAlts := parser! matchAlts false
+if (stx.getArg 1).isOfKind `Lean.Parser.Term.funMatchAlts then do
+  stxNew ← liftMacroM $ expandMatchAltsIntoMatch stx ((stx.getArg 1).getArg 1);
+  withMacroExpansion stx stxNew $ elabTerm stxNew expectedType?
+else do
+  let binders := (stx.getArg 1).getArgs;
+  let body := stx.getArg 3;
+  (binders, body, expandedPattern) ← expandFunBinders binders body;
+  if expandedPattern then do
+    newStx ← `(fun $binders* => $body);
+    withMacroExpansion stx newStx $ elabTerm newStx expectedType?
+  else
+    elabFunBinders binders expectedType? $ fun xs expectedType? => do
+      e ← elabTerm body expectedType?;
+      mkLambdaFVars xs e
+
 /- If `useLetExpr` is true, then a kernel let-expression `let x : type := val; body` is created.
    Otherwise, we create a term of the form `(fun (x : type) => body) val` -/
 def elabLetDeclAux (n : Name) (binders : Array Syntax) (typeStx : Syntax) (valStx : Syntax) (body : Syntax)

src/Lean/Elab/MutualDef.lean

@@ -295,7 +295,7 @@ let rec
     | x+1 => f x + z
 ```
 `y` is free variable in `f`, and `z` is a free variable in `g`.
-To close `f` and `g`, we `y` and `z` must be in the closure of both.
+To close `f` and `g`, `y` and `z` must be in the closure of both.
 That is, we need to generate the top-level definitions.
 ```
 def f (y z x : Nat) := g y z x + y

src/Lean/Parser/Term.lean

@@ -94,10 +94,6 @@ 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 funBinder : Parser := funImplicitBinder <|> instBinder <|> termParser maxPrec
-@[builtinTermParser] def «fun» := parser!:maxPrec unicodeSymbol "λ " "fun " >> many1 funBinder >> darrow >> termParser
-
 def matchAlt : Parser :=
 nodeWithAntiquot "matchAlt" `Lean.Parser.Term.matchAlt $
   sepBy1 termParser ", " >> darrow >> termParser
@@ -111,6 +107,12 @@ def matchDiscr := parser! optional (try (ident >> checkNoWsBefore "no space befo
 
 @[builtinTermParser] def «match» := parser!:leadPrec "match " >> sepBy1 matchDiscr ", " >> optType >> " with " >> matchAlts
 @[builtinTermParser] def «nomatch»  := parser!:leadPrec "nomatch " >> termParser
+
+def funImplicitBinder := try (lookahead ("{" >> many1 binderIdent >> (" : " <|> "}"))) >> implicitBinder
+def funBinder : Parser := funImplicitBinder <|> instBinder <|> termParser maxPrec
+def funMatchAlts := parser! matchAlts false
+@[builtinTermParser] def «fun» := parser!:maxPrec unicodeSymbol "λ " "fun " >> ((many1 funBinder >> darrow >> termParser) <|> funMatchAlts)
+
 def optExprPrecedence := optional (try ":" >> termParser maxPrec)
 @[builtinTermParser] def «parser!»  := parser!:leadPrec "parser! " >> optExprPrecedence >> termParser
 @[builtinTermParser] def «tparser!» := parser!:leadPrec "tparser! " >> optExprPrecedence >> termParser

tests/lean/run/match1.lean

@@ -0,0 +1,13 @@
+new_frontend
+
+def f (xs : List Nat) : List Bool :=
+xs.map fun
+  | 0 => true
+  | _ => false
+
+#eval f [1, 2, 0, 2]
+
+theorem ex1 : f [1, 0, 2] = [false, true, false] :=
+rfl
+
+#check f