test: document new test

pirapira · pirapira · commit 1c5fd4d50a16 · 2025-12-10T19:04:36.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
