hide solution

lean-ja · Mar 18, 2024 · d1714b4 · d1714b4
1 parent 8bdd948
commit d1714b4
Showing 1 changed file with 2 additions and 0 deletions.
diff --git a/Src/Problem11.lean b/Src/Problem11.lean
@@ -12,6 +12,7 @@ deriving Repr
 open Data
 
 def encodeModified (l : List α) : List (Data α) :=
+  -- sorry
   match l with
   | [] => []
   | x :: xs =>
@@ -20,6 +21,7 @@ def encodeModified (l : List α) : List (Data α) :=
       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.