chore: add failing grind test

2026-04-04 19:24:09 +00:00 · 2025-07-29 03:23:24 +02:00
1 changed files with 4 additions and 0 deletions
--- a/tests/lean/grind/algebra/linarith_cc.lean
+++ b/tests/lean/grind/algebra/linarith_cc.lean
@@ -0,0 +1,4 @@
+-- This fails unless we manually substitute `hb`.
+-- `grind` doesn't recognise this as a linear arithmetic problem.
+example (a : Nat) (ha : a < 8) (b : Nat) (hb : b = 2) : a * b < 8 * b := by
+  grind -- fails