From 59579bfc3e31c8da544d808eea6d073cd6ab53a2 Mon Sep 17 00:00:00 2001
From: Cameron Zwarich <cameron@lean-fro.org>
Date: Mon, 4 Aug 2025 12:47:40 -0700
Subject: [PATCH] refactor: remove `goBig` case from
 `UnreachableBranches.ofNat` (#9717)

This case can't meaningfully contribute to the result, because there are
no uses of `Nat` constructors in the `mono` phase.
---
 src/Lean/Compiler/LCNF/ElimDeadBranches.lean | 7 +------
 1 file changed, 1 insertion(+), 6 deletions(-)

diff --git a/src/Lean/Compiler/LCNF/ElimDeadBranches.lean b/src/Lean/Compiler/LCNF/ElimDeadBranches.lean
index 6a069ae45f..87facb7437 100644
--- a/src/Lean/Compiler/LCNF/ElimDeadBranches.lean
+++ b/src/Lean/Compiler/LCNF/ElimDeadBranches.lean
@@ -161,15 +161,10 @@ partial def getCtorArgs : Value → Name → Option (Array Value)
 
 partial def ofNat (n : Nat) : Value :=
   if n > maxValueDepth then
-    goBig n n
+    .top
   else
     goSmall n
 where
-  goBig (orig : Nat) (curr : Nat) : Value :=
-    if orig - curr == maxValueDepth then
-      .top
-    else
-      .ctor ``Nat.succ #[goBig orig (curr - 1)]
   goSmall : Nat → Value
   | 0 => .ctor ``Nat.zero #[]
   | n + 1 => .ctor ``Nat.succ #[goSmall n]