Skip to content

Commit 30fa545

Browse files
committed
chore: remove grind from Array.size_eq_zero_iff
1 parent 44ff700 commit 30fa545

File tree

1 file changed

+0
-1
lines changed

1 file changed

+0
-1
lines changed

src/Init/Data/Array/Lemmas.lean

Lines changed: 0 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -75,7 +75,6 @@ theorem ne_empty_of_size_pos (h : 0 < xs.size) : xs ≠ #[] := by
7575
cases xs
7676
simpa using List.ne_nil_of_length_pos h
7777

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

0 commit comments

Comments
 (0)