test: document new test

pirapira · pirapira · commit 181b8ea6d6ab · 2025-12-10T16:39:32.000+01:00
diff --git a/tests/playground/grind_div.lean b/tests/playground/grind_div.lean
@@ -1,3 +1,6 @@
 import Init.Data.Nat.Div.Basic
 
+/--
+This example tests the grind annotation on `mod_eq_of_lt`.
+-/
 example {a b : Nat} : a < b → a % b = a := by grind
