chore: add failing grind test

2026-04-05 03:34:08 +00:00 · 2025-04-11 05:01:42 +02:00
1 changed files with 4 additions and 0 deletions
--- a/tests/lean/grind/min.lean
+++ b/tests/lean/grind/min.lean
@@ -0,0 +1,4 @@
+example (as : Array α) (lo hi i j : Nat) (h₁ : lo ≤ i) (_ : i < j) (_ : j ≤ hi) (_ : j < as.size)
+    (_ : ¬as.size = 0) : min lo (as.size - 1) ≤ i := by
+  -- grind -- fails
+  omega