From 2528188ddeefed2c0e1b152d08f115c21f34bbf3 Mon Sep 17 00:00:00 2001 From: Kim Morrison Date: Fri, 11 Apr 2025 13:22:56 +1000 Subject: [PATCH] chore: add failing grind test (#7910) Adds a currently failing test, for a `grind` improvement. --- tests/lean/grind/min.lean | 4 ++++ 1 file changed, 4 insertions(+) create mode 100644 tests/lean/grind/min.lean diff --git a/tests/lean/grind/min.lean b/tests/lean/grind/min.lean new file mode 100644 index 0000000000..de5794fb2c --- /dev/null +++ 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