Skip to content

Commit 0d089e8

Browse files
committed
chore: fix tests
1 parent c9acac4 commit 0d089e8

File tree

2 files changed

+2
-2
lines changed

2 files changed

+2
-2
lines changed

tests/lean/run/grind_cutsat_trim_context.lean

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -12,4 +12,4 @@ open Lean Int Linear in
1212
set_option trace.grind.debug.proof true in
1313
example (f : Nat → Int) :
1414
f 1 <= 0 → f 2 <= 0 → f 3 <= 0 → f 4 <= 0 → f 5 <= 0 → f 6 <= 0 → f 7 <= 0 → f 8 <= 0 → -1 * f 2 + 1 <= 0 → False := by
15-
grind
15+
grind -order

tests/lean/run/grind_linarith_trim_context.lean

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -30,4 +30,4 @@ open Std Lean Grind Linarith in
3030
set_option trace.grind.debug.proof true in -- Context should contain only `f 2` and `One`
3131
example [CommRing α] [LE α] [LT α] [LawfulOrderLT α] [IsLinearOrder α] [OrderedRing α] (f : Nat → α) :
3232
f 1 <= 0 → f 2 <= 0 → f 3 <= 0 → f 4 <= 0 → f 5 <= 0 → f 6 <= 0 → f 7 <= 0 → f 8 <= 0 → -1 * f 2 + 1 <= 0 → False := by
33-
grind
33+
grind -order

0 commit comments

Comments
 (0)