update solutuion of P21

lean-ja · Mar 20, 2024 · 4cf28c7 · 4cf28c7
1 parent 8a730dc
commit 4cf28c7
Showing 1 changed file with 3 additions and 1 deletion.
diff --git a/Src/Problem21.lean b/Src/Problem21.lean
@@ -6,7 +6,9 @@ variable {α : Type}
 
 def insertAt (e : α) (l : List α) (i : Nat) : List α :=
   -- sorry
-  l.take (i - 1) ++ [e] ++ l.drop (i - 1)
+  match l, i with
+  | a :: b , i + 2 => a :: insertAt e b (i + 1)
+  | _ , _ => e :: l
   -- sorry
 
 -- The following code is a test case and you should not change it.