chore: grind only tests

leanprover · Jan 17, 2025 · 9fe4400 · 9fe4400
1 parent 63ce115
commit 9fe4400
Showing 1 changed file with 7 additions and 0 deletions.
diff --git a/tests/lean/run/grind_params.lean b/tests/lean/run/grind_params.lean
@@ -66,6 +66,13 @@ example : bla (bla (bla (bla x))) = bla x := by
   fail_if_success grind [-blathm]
   sorry
 
+example : bla (bla (bla (bla x))) = bla x := by
+  grind only [blathm]
+
+example : bla (bla (bla (bla x))) = bla x := by
+  fail_if_success grind only
+  sorry
+
 /--
 error: `pq` is not marked with the `[grind]` attribute
 -/