chore: remove grind from Array.size_eq_zero_iff

2026-04-10 06:04:09 +00:00 · 2025-05-24 14:00:28 +10:00
1 changed files with 0 additions and 1 deletions
--- a/src/Init/Data/Array/Lemmas.lean
+++ b/src/Init/Data/Array/Lemmas.lean
@@ -75,7 +75,6 @@ theorem ne_empty_of_size_pos (h : 0 < xs.size) : xs ≠ #[] := by
  cases xs
  simpa using List.ne_nil_of_length_pos h

-@[grind]
 theorem size_eq_zero_iff : xs.size = 0 ↔ xs = #[] :=
  ⟨eq_empty_of_size_eq_zero, fun h => h ▸ rfl⟩