From a22d8dd9245f445beee44f56d26b045013fa12f8 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Fri, 2 Apr 2021 07:29:56 -0700
Subject: [PATCH] fix: the code is reachable

---
 src/Lean/Elab/Match.lean | 8 ++++----
 1 file changed, 4 insertions(+), 4 deletions(-)

diff --git a/src/Lean/Elab/Match.lean b/src/Lean/Elab/Match.lean
index 17ec8acf4b..86a21c3b2c 100644
--- a/src/Lean/Elab/Match.lean
+++ b/src/Lean/Elab/Match.lean
@@ -138,14 +138,14 @@ def expandMacrosInPatterns (matchAlts : Array MatchAltView) : MacroM (Array Matc
 /- Given `stx` a match-expression, return its alternatives. -/
 private def getMatchAlts : Syntax → Array MatchAltView
   | `(match $discrs,* $[: $ty?]? with $alts:matchAlt*) =>
-    alts.map fun alt => match alt with
-      | `(matchAltExpr| | $patterns,* => $rhs) => {
+    alts.filterMap fun alt => match alt with
+      | `(matchAltExpr| | $patterns,* => $rhs) => some {
           ref      := alt,
           patterns := patterns,
           rhs      := rhs
         }
-      | _ => unreachable!
-  | _ => unreachable!
+      | _ => none
+  | _ => #[]
 
 /--
   Auxiliary annotation used to mark terms marked with the "inaccessible" annotation `.(t)` and