From f6fbba29eee089e1ea5a52e23a00bfd635d6a143 Mon Sep 17 00:00:00 2001
From: Seasawher <tellagoodstory@icloud.com>
Date: Mon, 25 Mar 2024 22:35:35 +0900
Subject: [PATCH] fix: namespace separation

---
 Src/Problem23.lean | 4 ++++
 Src/Problem24.lean | 4 ++++
 2 files changed, 8 insertions(+)

diff --git a/Src/Problem23.lean b/Src/Problem23.lean
index 7aa772f..82e2cd7 100644
--- a/Src/Problem23.lean
+++ b/Src/Problem23.lean
@@ -4,6 +4,8 @@
 -/
 import Lean
 
+namespace P23
+
 variable {α : Type} [Inhabited α]
 
 def rndSelect (l : List α) (n : Nat) : IO (List α) := do
@@ -40,3 +42,5 @@ def runTest [BEq α] [ToString α] (l : List α) (n : Nat) : IO Unit := do
 #eval runTest [2, 2, 2] 12
 
 #eval runTest (List.range 5200) 1897
+
+end P23
diff --git a/Src/Problem24.lean b/Src/Problem24.lean
index 6fa0ddd..ca87efa 100644
--- a/Src/Problem24.lean
+++ b/Src/Problem24.lean
@@ -4,6 +4,8 @@
 -/
 import Lean
 
+namespace P24
+
 /-- List of natural numbers from `1` to `n` -/
 def List.nrange (n : Nat) : List Nat :=
   match n with
@@ -65,3 +67,5 @@ def runTest (count range : Nat) : IO Unit := do
 #eval runTest 1998 1999
 
 #eval runTest 5668 5998
+
+end P24