From b9bfd305143a4cca11760bb8b2fdf82bd50f2ae9 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Henrik=20B=C3=B6ving?= <hargonix@gmail.com>
Date: Thu, 6 Jun 2024 20:04:55 +0200
Subject: [PATCH] chore: remove partial TODO (#4380)

---
 src/Lean/Level.lean | 3 +--
 1 file changed, 1 insertion(+), 2 deletions(-)

diff --git a/src/Lean/Level.lean b/src/Lean/Level.lean
index d6f0d609bf..40d8998897 100644
--- a/src/Lean/Level.lean
+++ b/src/Lean/Level.lean
@@ -258,8 +258,7 @@ def ctorToNat : Level → Nat
   | max ..   => 4
   | imax ..  => 5
 
-/- TODO: use well founded recursion. -/
-partial def normLtAux : Level → Nat → Level → Nat → Bool
+def normLtAux : Level → Nat → Level → Nat → Bool
   | succ l₁, k₁, l₂, k₂ => normLtAux l₁ (k₁+1) l₂ k₂
   | l₁, k₁, succ l₂, k₂ => normLtAux l₁ k₁ l₂ (k₂+1)
   | l₁@(max l₁₁ l₁₂), k₁, l₂@(max l₂₁ l₂₂), k₂ =>