From 4e209effe5c38bb592c11e4ad06f7796980175cc Mon Sep 17 00:00:00 2001
From: "F. G. Dorais" <fgdorais@gmail.com>
Date: Fri, 25 Oct 2024 17:23:01 -0400
Subject: [PATCH] chore: cleanup

---
 Batteries/Data/Fin/Basic.lean | 9 ---------
 1 file changed, 9 deletions(-)

diff --git a/Batteries/Data/Fin/Basic.lean b/Batteries/Data/Fin/Basic.lean
index 39db490057..e3970e08c9 100644
--- a/Batteries/Data/Fin/Basic.lean
+++ b/Batteries/Data/Fin/Basic.lean
@@ -84,15 +84,6 @@ protected def count (P : Fin n → Prop) [DecidablePred P] : Nat :=
 /-- Find the first true value of a decidable predicate on `Fin n`, if there is one. -/
 protected def find? (P : Fin n → Prop) [DecidablePred P] : Option (Fin n) :=
   foldr n (fun i v => if P i then some i else v) none
-  -- match n, P, inst with
-  -- | 0, _, _ => none
-  -- | _+1, P, _ =>
-  --   if P 0 then
-  --     some 0
-  --   else
-  --     match Fin.find? fun i => P i.succ with
-  --     | some i => some i.succ
-  --     | none => none
 
 /-- Custom recursor for `Fin (n+1)`. -/
 def recZeroSuccOn {motive : Fin (n+1) → Sort _} (x : Fin (n+1))