fix: namespace separation

lean-ja · Mar 25, 2024 · f6fbba2 · f6fbba2
1 parent 01fbbe1
commit f6fbba2
Show file tree

Hide file tree

Showing 2 changed files with 8 additions and 0 deletions.
diff --git 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
@@ -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