edit message

Src/Problem1.lean

@@ -12,7 +12,7 @@ def myLast (l : List α) : Option α :=
   | _ :: as => myLast as
   -- sorry
 
--- The following code is a test case and you should not change it.
+-- The following codes are for test and you should not edit these.
 
 example : myLast [1, 2, 3, 4] = some 4 := by rfl
 

Src/Problem10.lean

@@ -24,7 +24,7 @@ def encode (l : List α) : List (Nat × α) :=
   pack l |>.map fun x => (x.length, x.head!)
   -- sorry
 
--- The following code is a test case and you should not change it.
+-- The following codes are for test and you should not edit these.
 
 example : encode [1, 1, 2, 2, 2, 3, 4, 4, 4, 4] = [(2, 1), (3, 2), (1, 3), (4, 4)] := rfl
 

Src/Problem11.lean

@@ -30,7 +30,7 @@ def encodeModified (l : List α) : List (Data α) :=
   decreasing_by
     all_goals sorry
 
--- The following code is a test case and you should not change it.
+-- The following codes are for test and you should not edit these.
 
 example : encodeModified ['a', 'a', 'b', 'c'] =
   [multiple 2 'a', single 'b', single 'c'] := by rfl

Src/Problem12.lean

@@ -21,7 +21,7 @@ def decodeModified (l : List (Data α)) : List α :=
   | (single a) :: t => a :: decodeModified t
   -- sorry
 
--- The following code is a test case and you should not change it.
+-- The following codes are for test and you should not edit these.
 
 example : decodeModified [multiple 2 'a', single 'b', multiple 2 'c'] = ['a', 'a', 'b', 'c', 'c'] := rfl
 

Src/Problem13.lean

@@ -32,7 +32,7 @@ where
       (n + 1, a) :: (counting (b :: t) |>.tail!)
   -- sorry
 
--- The following code is a test case and you should not change it.
+-- The following codes are for test and you should not edit these.
 
 example : encodeDirect ['a', 'a', 'b', 'c'] =
   [multiple 2 'a', single 'b', single 'c'] := by rfl

Src/Problem14.lean

@@ -12,7 +12,7 @@ def dupli (l : List α) : List α :=
   | a :: b => a :: a :: dupli b
   -- sorry
 
--- The following code is a test case and you should not change it.
+-- The following codes are for test and you should not edit these.
 
 example : dupli [1, 2, 3] = [1, 1, 2, 2, 3, 3] := by rfl
 

Src/Problem15.lean

@@ -16,7 +16,7 @@ def repli (l : List α) (n : Nat) : List α :=
     | m + 1 => x :: solorepl x m
   -- sorry
 
--- The following code is a test case and you should not change it.
+-- The following codes are for test and you should not edit these.
 
 example : repli [1, 2, 3] 3 = [1, 1, 1, 2, 2, 2, 3, 3, 3] := by rfl
 

Src/Problem16.lean

@@ -17,7 +17,7 @@ where
       x :: helper xs n (m + 1)
   -- sorry
 
--- The following code is a test case and you should not change it.
+-- The following codes are for test and you should not edit these.
 
 example : dropEvery [1, 2, 3] 0 = [1, 2, 3] := by rfl
 

Src/Problem17.lean

@@ -18,7 +18,7 @@ def split (l : List α) (n : Nat) : List α × List α :=
     (h :: a, b)
   -- sorry
 
--- The following code is a test case and you should not change it.
+-- The following codes are for test and you should not edit these.
 
 example : split [1, 2, 3, 4, 5] 2 = ([1, 2], [3, 4, 5]) := rfl
 

Src/Problem18.lean

@@ -12,7 +12,7 @@ def slice (l : List α) (i k : Nat) : List α :=
     l.drop (k - 1) |>.take (i - k + 1)
   -- sorry
 
--- The following code is a test case and you should not change it.
+-- The following codes are for test and you should not edit these.
 
 example : slice [1, 2, 3, 4, 5, 6, 7, 8, 9] 3 7 = [3, 4, 5, 6, 7] := by rfl
 

Src/Problem19.lean

@@ -10,7 +10,7 @@ def rotate (l : List α) (n : Nat) : List α :=
   l.drop n ++ l.take n
   -- sorry
 
--- The following code is a test case and you should not change it.
+-- The following codes are for test and you should not edit these.
 
 example : rotate [1, 2, 3, 4, 5] 2 = [3, 4, 5, 1, 2] := rfl
 

Src/Problem2.lean

@@ -15,7 +15,7 @@ def myButLast (l : List α) : Option α :=
     | none => none
   -- sorry
 
--- The following code is a test case and you should not change it.
+-- The following codes are for test and you should not edit these.
 
 example : myButLast [1, 2, 3, 4] = some 3 := rfl
 

Src/Problem20.lean

@@ -13,7 +13,7 @@ def removeAt (l : List α) (n : Nat) : List α :=
   | x :: b, m + 2 => x :: removeAt b (m + 1)
   -- sorry
 
--- The following code is a test case and you should not change it.
+-- The following codes are for test and you should not edit these.
 
 example : removeAt ['a', 'b', 'c', 'd'] 2 = ['a', 'c', 'd'] := rfl
 

Src/Problem21.lean

@@ -11,7 +11,7 @@ def insertAt (e : α) (l : List α) (i : Nat) : List α :=
   | _ , _ => e :: l
   -- sorry
 
--- The following code is a test case and you should not change it.
+-- The following codes are for test and you should not edit these.
 
 example : insertAt "X" ["1", "2", "3", "4"] 2 = ["1", "X", "2", "3", "4"] := rfl
 

Src/Problem22.lean

@@ -13,7 +13,7 @@ where
     | l + 1 => generate start l ++ [start + l]
   -- sorry
 
--- The following code is a test case and you should not change it.
+-- The following codes are for test and you should not edit these.
 
 example : range 4 9 = [4, 5, 6, 7, 8, 9] := by rfl
 

Src/Problem23.lean

@@ -17,7 +17,7 @@ def rndSelect (l : List α) (n : Nat) : IO (List α) := do
     pure <| l[index]! :: previous
   -- sorry
 
--- The following code is a test case and you should not change it.
+-- The following codes are for test and you should not edit these.
 
 def runTest (l : List Nat) (n : Nat) : IO Unit := do
   let result ← rndSelect l n

Src/Problem24.lean

@@ -42,7 +42,7 @@ where
     return (element, rest)
   -- sorry
 
--- The following code is a test case and you should not change it.
+-- The following codes are for test and you should not edit these.
 
 def runTest (count range : Nat) : IO Unit := do
   let result ← diffSelect count range

Src/Problem3.lean

@@ -13,7 +13,7 @@ def elementAt (l : List α) (k : Nat) : Option α :=
   | _ :: a, k + 1 => elementAt a k
   -- sorry
 
--- The following code is a test case and you should not change it.
+-- The following codes are for test and you should not edit these.
 
 example : elementAt ['a', 'b', 'c', 'd', 'e'] 3 = some 'c' := by rfl
 

Src/Problem31.lean

@@ -18,7 +18,7 @@ def isPrime (n : Nat) : Bool :=
     divList.length == 0
   -- sorry
 
--- The following code is a test case and you should not change it.
+-- The following codes are for test and you should not edit these.
 
 example : isPrime 7 = true := rfl
 

Src/Problem32.lean

@@ -16,7 +16,7 @@ def gcd (m n : Nat) : Nat :=
   -- You don't have to fill in the `sorry` here.
   decreasing_by sorry
 
--- The following code is a test case and you should not change it.
+-- The following codes are for test and you should not edit these.
 
 example : gcd 6 0 = 6 := by first | native_decide | rfl
 

Src/Problem4.lean

@@ -11,7 +11,7 @@ def myLength (l : List α) : Nat :=
   | _ :: a => myLength a + 1
   -- sorry
 
--- The following code is a test case and you should not change it.
+-- The following codes are for test and you should not edit these.
 
 example : myLength [123, 456, 789] = 3 := by rfl
 

Src/Problem5.lean

@@ -11,7 +11,7 @@ def myReverse (l : List α) : List α :=
   | a :: as => myReverse as ++ [a]
   -- sorry
 
--- The following code is a test case and you should not change it.
+-- The following codes are for test and you should not edit these.
 
 example : myReverse [1, 2, 3, 4] = [4, 3, 2, 1] := rfl
 

Src/Problem6.lean

@@ -18,7 +18,7 @@ def isPalindrome (l : List α) : Bool :=
   l == l.reverse
   -- sorry
 
--- The following code is a test case and you should not change it.
+-- The following codes are for test and you should not edit these.
 
 example : isPalindrome [1, 2, 3] = false := rfl
 

Src/Problem7.lean

@@ -53,7 +53,7 @@ def flatten (nl : NestedList α) : List α :=
   | list (x :: xs) => flatten x ++ flatten (list xs)
   -- sorry
 
--- The following code is a test case and you should not change it.
+-- The following codes are for test and you should not edit these.
 
 example : flatten (elem 5) = [5] := rfl
 

Src/Problem8.lean

@@ -19,7 +19,7 @@ def compress (l : List α) : List α :=
         a' :: comp' l' a'
   -- sorry
 
--- The following code is a test case and you should not change it.
+-- The following codes are for test and you should not edit these.
 
 example : compress [1, 1, 2, 2, 1, 2, 2] = [1, 2, 1, 2] := by rfl
 

Src/Problem9.lean

@@ -19,7 +19,7 @@ def pack (l : List α) : List (List α) :=
   -- You don't have to fill in the `sorry` here.
   decreasing_by sorry
 
--- The following code is a test case and you should not change it.
+-- The following codes are for test and you should not edit these.
 
 example : pack ([] : List α) = [] := rfl