From d1714b45cf5561cbbc5e97fe201174f5307d2407 Mon Sep 17 00:00:00 2001 From: Seasawher Date: Mon, 18 Mar 2024 22:11:58 +0900 Subject: [PATCH] hide solution --- Src/Problem11.lean | 2 ++ 1 file changed, 2 insertions(+) diff --git a/Src/Problem11.lean b/Src/Problem11.lean index 04b5c18..abd748f 100644 --- 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.