chore: missing modifier

2026-03-26 14:54:15 +00:00 · 2025-09-18 07:36:53 -07:00
1 changed files with 1 additions and 1 deletions
--- a/src/Init/Data/ByteArray/Lemmas.lean
+++ b/src/Init/Data/ByteArray/Lemmas.lean
@@ -81,7 +81,7 @@ theorem ByteArray.append_empty {b : ByteArray} : b ++ ByteArray.empty = b := by
  ext1
  simp

-@[simp, grind]
+@[simp, grind =]
 theorem ByteArray.size_append {a b : ByteArray} : (a ++ b).size = a.size + b.size := by
  simp [← size_data]