chore: remove confusing test

geezer-workshop · Sep 13, 2024 · 5f789e6 · 5f789e6
1 parent 438061a
commit 5f789e6
Showing 1 changed file with 0 additions and 6 deletions.
diff --git a/tests/lean/linterUnusedVariables.lean b/tests/lean/linterUnusedVariables.lean
@@ -250,12 +250,6 @@ example [ord : Ord β] (f : α → β) (x y : α) : Ordering := compare (f x) (f
 example {α β} [ord : Ord β] (f : α → β) (x y : α) : Ordering := compare (f x) (f y)
 example {h : Decidable True} (t e : α) : ite True t e = t := if_pos trivial
 
-@[unused_variables_ignore_fn]
-def ignoreEverything : Lean.Linter.IgnoreFunction :=
-  fun _ _ _ => true
-
-def ignored (x : Nat) := 0
-
 /-!
 The wildcard pattern introduces a copy of `x` that should not be linted as it is in an
 inaccessible annotation.