test: add test for new grind annotation

pirapira · pirapira · commit 7e8695cde1d1 · 2025-12-10T16:26:26.000+01:00
diff --git a/tests/playground/grind_div.lean b/tests/playground/grind_div.lean
@@ -0,0 +1,3 @@
+import Init.Data.Nat.Div.Basic
+
+example {a b : Nat} : a < b → a % b = a := by grind

Original file line number	Diff line number	Diff line change
`@@ -0,0 +1,3 @@`
	`1`	`+import Init.Data.Nat.Div.Basic`
	`2`	`+`
	`3`	`+example {a b : Nat} : a < b → a % b = a := by grind`