P2: Functor.map を使用しない

lean-ja · Apr 21, 2024 · fbae9d6 · fbae9d6
1 parent fdd41f1
commit fbae9d6
Showing 1 changed file with 3 additions and 1 deletion.
diff --git a/Src/Problem2.lean b/Src/Problem2.lean
@@ -12,7 +12,9 @@ def myButLast (l : List α) : Option α :=
     none
   else
     let i := l.length - 2;
-    id <$> l[i]?
+    match l[i]? with
+    | some x => some x
+    | none => none
   -- sorry
 
 -- The following codes are for test and you should not edit these.