test

Author: leodemoura

tests/lean/run/grind_linarith_2.lean

@@ -64,3 +64,15 @@ example [CommRing α] [LinearOrder α] [Ring.IsOrdered α] (a b c : α)
 example [CommRing α] [LinearOrder α] [Ring.IsOrdered α] (a b c : α)
     : c = a → a + b ≤ 3 → 3 ≤ b + c → a + b = 3 := by
   grind
+
+/--
+trace: [grind.linarith.model] a := 7/2
+[grind.linarith.model] b := 1
+[grind.linarith.model] c := 2
+[grind.linarith.model] d := 3
+-/
+#guard_msgs (drop error, trace) in
+set_option trace.grind.linarith.model true in
+example [CommRing α] [LinearOrder α] [Ring.IsOrdered α] (a b c d : α)
+    : b ≥ 0 → c > b → d > b → a ≠ b + c → a > b + c → a < b + d →  False := by
+  grind