comment

leanprover · Jan 15, 2025 · d53c45e · d53c45e
1 parent 70b979a
commit d53c45e
Showing 1 changed file with 1 addition and 0 deletions.
diff --git a/src/Init/Data/Nat/Lemmas.lean b/src/Init/Data/Nat/Lemmas.lean
@@ -1025,6 +1025,7 @@ theorem mul_add_mod (m x y : Nat) : (m * x + y) % m = y % m := by
 
 instance decidableBallLT (n : Nat) (P : ∀ k, k < n → Prop) [H : ∀ n h, Decidable (P n h)] :
     Decidable (∀ n h, P n h) :=
+  -- tail-recursion doesn't save stack frames in kernel reduction, so we also need a nested loop
   let rec inner : ∀ n1 ≤ n, ∀ n2 ≤ n1, (∀ n h, n1 ≤ n → P n h) → Decidable (∀ n h, n2 ≤ n → P n h)
     | 0, _, _, _, h2 => isTrue fun n' hn' _ => h2 n' hn' (Nat.zero_le _)
     | n1 + 1, h1, n2, hn2, h2 =>