remove some using coercion

lean-ja · Mar 24, 2024 · b7551c0 · b7551c0
1 parent 2ba6f4f
commit b7551c0
Show file tree

Hide file tree

Showing 3 changed files with 3 additions and 3 deletions.
diff --git a/Src/Problem1.lean b/Src/Problem1.lean
@@ -8,7 +8,7 @@ def myLast (l : List α) : Option α :=
   -- sorry
   match l with
   | [] => none
-  | [a] => some a
+  | [a] => a
   | _ :: as => myLast as
   -- sorry
 

diff --git a/Src/Problem2.lean b/Src/Problem2.lean
@@ -11,7 +11,7 @@ def myButLast (l : List α) : Option α :=
   else
     let i := l.length - 2;
     match l[i]? with
-    | some x => some x
+    | some x => x
     | none => none
   -- sorry
 

diff --git a/Src/Problem3.lean b/Src/Problem3.lean
@@ -9,7 +9,7 @@ def elementAt (l : List α) (k : Nat) : Option α :=
   match l, k with
   | [], _ => none
   | _, 0 => none
-  | a :: _, 1 => some a
+  | a :: _, 1 => a
   | _ :: a, k + 1 => elementAt a k
   -- sorry