From 19a50a32ecaee4013dc149f85381fac4e4d41477 Mon Sep 17 00:00:00 2001
From: Mario Carneiro <di.gama@gmail.com>
Date: Sat, 10 Sep 2022 20:19:37 -0400
Subject: [PATCH] chore: remove List.init

---
 src/Init/Data/List/Basic.lean | 5 -----
 1 file changed, 5 deletions(-)

diff --git a/src/Init/Data/List/Basic.lean b/src/Init/Data/List/Basic.lean
index 38e9afe3ad..b6f57cd777 100644
--- a/src/Init/Data/List/Basic.lean
+++ b/src/Init/Data/List/Basic.lean
@@ -404,11 +404,6 @@ def enumFrom : Nat → List α → List (Nat × α)
 
 def enum : List α → List (Nat × α) := enumFrom 0
 
-def init : List α → List α
-  | []   => []
-  | [_]  => []
-  | a::l => a::init l
-
 def intersperse (sep : α) : List α → List α
   | []    => []
   | [x]   => [x]