update test

leanprover · Jul 28, 2024 · 51f6243 · 51f6243
1 parent 1d4efa7
commit 51f6243
Showing 1 changed file with 0 additions and 4 deletions.
diff --git a/tests/lean/run/starsAndBars.lean b/tests/lean/run/starsAndBars.lean
@@ -1,7 +1,3 @@
-@[simp] def List.count [DecidableEq α] : List α → α → Nat
-  | [], _    => 0
-  | a::as, b => if a = b then as.count b + 1 else as.count b
-
 inductive StarsAndBars : Nat → Nat → Type where
   | nil  : StarsAndBars 0 0
   | star : StarsAndBars s b → StarsAndBars (s+1) b