fix solution of P35

lean-ja · Apr 10, 2024 · 9835ccc · 9835ccc
1 parent 17658c6
commit 9835ccc
Showing 1 changed file with 3 additions and 1 deletion.
diff --git a/Src/Problem35.lean b/Src/Problem35.lean
@@ -9,7 +9,9 @@ def primeFactors (n : Nat) : List Nat :=
   -- sorry
   loop n 2 [] |>.reverse
   where loop (tgt candidate : Nat) (acc : List Nat) : List Nat :=
-    if candidate <= 1 || tgt ≤ 1 then
+    if candidate <= 1 || candidate > tgt then
+      panic! "candidate is out of range"
+    else if tgt ≤ 1 then
       acc
     else if tgt % candidate = 0 then
       loop (tgt / candidate) candidate <| candidate :: acc