test: from Kim's test suite

leanprover · Jan 13, 2025 · 076d7f8 · 076d7f8
1 parent 7f46b84
commit 076d7f8
Showing 1 changed file with 6 additions and 0 deletions.
diff --git a/tests/lean/run/grind_t1.lean b/tests/lean/run/grind_t1.lean
@@ -263,3 +263,9 @@ a✝ : p
 set_option trace.grind.split true in
 example (p q : Prop) : ¬(p ↔ q) → p → False := by
   grind -- should not split on (p ↔ q)
+
+example {a b : Nat} (h : a < b) : ¬ b < a := by
+  grind
+
+example {m n : Nat} : m < n ↔ m ≤ n ∧ ¬ n ≤ m := by
+  grind