From 2e11053eb5280268171a892ae7abeae0c5570cff Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Tue, 8 Sep 2020 17:31:57 -0700
Subject: [PATCH] fix: `matchAlt` macros should not consume implicit arguments
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

As in Lean3, the following example is a valid definition

```
def head : {α : Type} → List α → Option α
| _, a::as => some a
| _, _     => none
```
---
 src/Lean/Elab/Binders.lean |  2 +-
 tests/lean/run/match1.lean | 24 ++++++++++++++++++++++++
 2 files changed, 25 insertions(+), 1 deletion(-)

diff --git a/src/Lean/Elab/Binders.lean b/src/Lean/Elab/Binders.lean
index 0607fbf884..0532b3fa34 100644
--- a/src/Lean/Elab/Binders.lean
+++ b/src/Lean/Elab/Binders.lean
@@ -390,7 +390,7 @@ private def expandMatchAltsIntoMatchAux (ref : Syntax) (matchAlts : Syntax) (mat
   if matchTactic then
     `(tactic| intro $x:term; $body:tactic)
   else
-    `(fun $x => $body)
+    `(@fun $x => $body)
 
 /--
   Expand `matchAlts` syntax into a full `match`-expression.
diff --git a/tests/lean/run/match1.lean b/tests/lean/run/match1.lean
index aae7cb8cd6..f84ebb440f 100644
--- a/tests/lean/run/match1.lean
+++ b/tests/lean/run/match1.lean
@@ -34,3 +34,27 @@ inductive C
 def C.x : C → Nat
 | C.mk₁ x   => x
 | C.mk₂ x _ => x
+
+def head : {α : Type} → List α → Option α
+| _, a::as => some a
+| _, _     => none
+
+theorem ex4 : head [1, 2] = some 1 :=
+rfl
+
+def head2 : {α : Type} → List α → Option α :=
+@fun
+  | _, a::as => some a
+  | _, _     => none
+
+theorem ex5 : head2 [1, 2] = some 1 :=
+rfl
+
+def head3 {α : Type} (xs : List α) : Option α :=
+let rec aux : {α : Type} → List α → Option α
+  | _, a::as => some a
+  | _, _     => none;
+aux xs
+
+theorem ex6 : head3 [1, 2] = some 1 :=
+rfl