From 85a1a5233bfa69f418f6ca333c50f7e26fa368d8 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Tue, 1 Mar 2022 08:35:00 -0800
Subject: [PATCH] chore: workaround for compiler closed term extraction issue

---
 src/Lean/Compiler/IR/SimpCase.lean | 5 ++++-
 1 file changed, 4 insertions(+), 1 deletion(-)

diff --git a/src/Lean/Compiler/IR/SimpCase.lean b/src/Lean/Compiler/IR/SimpCase.lean
index 5a6042c84e..8a8cb2a806 100644
--- a/src/Lean/Compiler/IR/SimpCase.lean
+++ b/src/Lean/Compiler/IR/SimpCase.lean
@@ -43,8 +43,11 @@ private def addDefault (alts : Array Alt) : Array Alt :=
       let alts := alts.filter fun alt => alt.body != max.body
       alts.push (Alt.default max.body)
 
+private def filterUnreachable (alts : Array Alt) : Array Alt :=
+  alts.filter fun alt => alt.body != FnBody.unreachable
+
 private def mkSimpCase (tid : Name) (x : VarId) (xType : IRType) (alts : Array Alt) : FnBody :=
-  let alts := alts.filter (fun alt => alt.body != FnBody.unreachable);
+  let alts := filterUnreachable alts
   let alts := addDefault alts;
   if alts.size == 0 then
     FnBody.unreachable