remove decreasing_by

Src/Problem11.lean

@@ -9,35 +9,30 @@ variable {α : Type} [BEq α]
 inductive Data (α : Type) where
   | multiple : Nat → α → Data α
   | single : α → Data α
-deriving Repr
+deriving Repr, DecidableEq
 
 open Data
 
-def encodeModified (l : List α) : List (Data α) :=
+partial def encodeModified (l : List α) : List (Data α) :=
   -- sorry
   match l with
   | [] => []
-  | x :: xs =>
+  | x :: _xs =>
     let (as, bs) := l.span (· == x)
     if as.length > 1 then
       multiple as.length x :: encodeModified bs
     else
       single x :: encodeModified bs
   -- sorry
 
-  -- Avoid proving that the function terminates as a recursive function.
-  -- You don't have to fill in the `sorry` here.
-  decreasing_by
-    all_goals sorry
-
 -- 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
+  [multiple 2 'a', single 'b', single 'c'] := by native_decide
 
-example : encodeModified ([] : List α) = [] := by rfl
+example : encodeModified ([] : List Nat) = [] := by native_decide
 
 example : encodeModified ['a', 'b', 'b', 'b', 'c', 'b', 'b'] =
-  [single 'a', multiple 3 'b', single 'c', multiple 2 'b'] := by rfl
+  [single 'a', multiple 3 'b', single 'c', multiple 2 'b'] := by native_decide
 
 end P11 --#

Src/Problem32.lean

@@ -7,18 +7,14 @@
 #check Nat.gcd
 
 /-- Euclidean algorithm -/
-def gcd (m n : Nat) : Nat :=
+partial def gcd (m n : Nat) : Nat :=
   -- sorry
   if m = 0 then
     n
   else
     gcd (n % m) m
   -- sorry
 
-  -- Avoid proving that the function terminates as a recursive function.
-  -- You don't have to fill in the `sorry` here.
-  decreasing_by sorry
-
 -- The following codes are for test and you should not edit these.
 
 example : gcd 6 0 = 6 := by native_decide

Src/Problem35.lean

@@ -5,7 +5,7 @@
 Construct a flat list containing the prime factors in ascending order.
 -/
 
-def primeFactors (n : Nat) : List Nat :=
+partial def primeFactors (n : Nat) : List Nat :=
   -- sorry
   loop n 2 [] |>.reverse
 where
@@ -16,8 +16,6 @@ where
       loop (tgt / candidate) candidate <| candidate :: acc
     else
       loop tgt (candidate + 1) acc
-
-    decreasing_by all_goals sorry
   -- sorry
 
 -- The following codes are for test and you should not edit these.