From d2f1919263fbde09514739ecdf0b814ce1a4f426 Mon Sep 17 00:00:00 2001 From: csharpython <121863991+csharpython@users.noreply.github.com> Date: Sun, 17 Mar 2024 18:53:40 +0900 Subject: [PATCH] Update Problem4.lean MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit 不要な場合分けの修正 --- Src/Problem4.lean | 1 - 1 file changed, 1 deletion(-) diff --git a/Src/Problem4.lean b/Src/Problem4.lean index 0078aff..7c6985b 100644 --- a/Src/Problem4.lean +++ b/Src/Problem4.lean @@ -9,7 +9,6 @@ def myLength (l : List α) : Nat := -- sorry match l with | [] => 0 - | [_] => 1 | _ :: a => (myLength a).succ -- sorry