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]