Skip to content

Commit

Permalink
update P23: generalize test code
Browse files Browse the repository at this point in the history
  • Loading branch information
Seasawher committed Mar 25, 2024
1 parent 145beda commit 01fbbe1
Showing 1 changed file with 3 additions and 1 deletion.
4 changes: 3 additions & 1 deletion Src/Problem23.lean
Original file line number Diff line number Diff line change
Expand Up @@ -19,7 +19,7 @@ def rndSelect (l : List α) (n : Nat) : IO (List α) := do

-- The following codes are for test and you should not edit these.

def runTest (l : List Nat) (n : Nat) : IO Unit := do
def runTest [BEq α] [ToString α] (l : List α) (n : Nat) : IO Unit := do
let result ← rndSelect l n
let mut check := true
check := check && result.length == n
Expand All @@ -31,6 +31,8 @@ def runTest (l : List Nat) (n : Nat) : IO Unit := do

#eval runTest [1, 2, 3] 0

#eval runTest ['a', 'b'] 1

#eval runTest [1, 2, 3, 4, 5] 2

#eval runTest [1, 1, 1] 2
Expand Down

0 comments on commit 01fbbe1

Please sign in to comment.