From 78a8bc7b7eeb93b5b9dbe005672fd3e78f93baee Mon Sep 17 00:00:00 2001
From: Sebastian Ullrich <sebasti@nullri.ch>
Date: Tue, 27 Oct 2020 15:22:54 +0100
Subject: [PATCH] feat: adapt elaborator to preceding change

---
 src/Lean/Elab/Binders.lean | 14 ++++++--------
 src/Lean/Parser/Term.lean  |  2 +-
 2 files changed, 7 insertions(+), 9 deletions(-)

diff --git a/src/Lean/Elab/Binders.lean b/src/Lean/Elab/Binders.lean
index d0b8639dc8..b0e94c2b9a 100644
--- a/src/Lean/Elab/Binders.lean
+++ b/src/Lean/Elab/Binders.lean
@@ -401,14 +401,8 @@ def expandMatchAltsIntoMatch (ref : Syntax) (matchAlts : Syntax) (tactic := fals
 def expandMatchAltsIntoMatchTactic (ref : Syntax) (matchAlts : Syntax) : MacroM Syntax :=
   expandMatchAltsIntoMatchAux ref matchAlts true (getMatchAltNumPatterns matchAlts) #[]
 
-@[builtinTermElab «fun»] def elabFun : TermElab := fun stx expectedType? => do
-  -- "fun " >> ((many1 funBinder >> darrow >> termParser) <|> matchAlts)
-  if stx[1].isOfKind `Lean.Parser.Term.matchAlts then
-    let stxNew ← liftMacroM $ expandMatchAltsIntoMatch stx stx[1]
-    withMacroExpansion stx stxNew $ elabTerm stxNew expectedType?
-  else
-    let binders := stx[1].getArgs
-    let body := stx[3]
+@[builtinTermElab «fun»] def elabFun : TermElab := fun stx expectedType? => match_syntax stx with
+  | `(fun $binders* => $body) => do
     let (binders, body, expandedPattern) ← expandFunBinders binders body
     if expandedPattern then
       let newStx ← `(fun $binders* => $body)
@@ -420,6 +414,10 @@ def expandMatchAltsIntoMatchTactic (ref : Syntax) (matchAlts : Syntax) : MacroM
            and another instance for the dependent version. -/
         let e ← elabTermEnsuringType body expectedType?
         mkLambdaFVars xs e
+  | `(fun $m:matchAlts) => do
+    let stxNew ← liftMacroM $ expandMatchAltsIntoMatch stx m
+    withMacroExpansion stx stxNew $ elabTerm stxNew expectedType?
+  | _ => throwUnsupportedSyntax
 
 /- 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`
diff --git a/src/Lean/Parser/Term.lean b/src/Lean/Parser/Term.lean
index 88671cb0da..8ce02bb0e4 100644
--- a/src/Lean/Parser/Term.lean
+++ b/src/Lean/Parser/Term.lean
@@ -141,7 +141,7 @@ def funImplicitBinder := «try» (lookahead ("{" >> many1 binderIdent >> (" : "
 def funBinder : Parser := funImplicitBinder <|> instBinder <|> termParser maxPrec
 -- NOTE: we use `nodeWithAntiquot` to ensure that `fun $b => ...` remains a `term` antiquotation
 def basicFun : Parser := nodeWithAntiquot "basicFun" `Lean.Parser.Term.basicFun (many1 (ppSpace >> funBinder) >> darrow >> termParser)
-@[builtinTermParser] def «fun» := parser!:maxPrec unicodeSymbol "λ" "fun" >> (checkInsideQuot >> basicFun <|> checkOutsideQuot >> (many1 (ppSpace >> funBinder) >> darrow >> termParser) <|> matchAlts false)
+@[builtinTermParser] def «fun» := parser!:maxPrec unicodeSymbol "λ" "fun" >> (basicFun <|> matchAlts false)
 
 def optExprPrecedence := optional («try» ":" >> termParser maxPrec)
 @[builtinTermParser] def «parser!»  := parser!:leadPrec "parser! " >> optExprPrecedence >> termParser