update P24: use statement-like expression in do block

lean-ja · Mar 24, 2024 · 92637c6 · 92637c6
1 parent 63c7e72
commit 92637c6
Showing 1 changed file with 8 additions and 9 deletions.
diff --git a/Src/Problem24.lean b/Src/Problem24.lean
@@ -28,18 +28,17 @@ def diffSelect (count range : Nat) : IO (List Nat) := do
     if let some e := element then
       univ := rest
       result := e :: result
-    else
-      break
+
   return result
 where
   extractOne (univ : List Nat) : IO (Option Nat × List Nat) := do
-    match univ with
-    | [] => pure (none, [])
-    | _ =>
-      let index ← IO.rand 0 (univ.length - 1)
-      let element := univ.get! index
-      let rest := univ.take index ++ univ.drop (index + 1)
-      pure (element, rest)
+    if univ == [] then
+      return (none, [])
+
+    let index ← IO.rand 0 (univ.length - 1)
+    let element := univ.get! index
+    let rest := univ.take index ++ univ.drop (index + 1)
+    return (element, rest)
   -- sorry
 
 #eval diffSelect 3 3