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.
This commit is contained in:
Cameron Zwarich 2025-08-04 12:47:40 -07:00 committed by GitHub
parent 7f22c0883b
commit 59579bfc3e
No known key found for this signature in database
GPG key ID: B5690EEEBB952194

View file

@ -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]