We read every piece of feedback, and take your input very seriously.
To see all available qualifiers, see our documentation.
There was an error while loading. Please reload this page.
1 parent 11f88a4 commit 7429773Copy full SHA for 7429773
tests/lean/run/grind_offset_cnstr.lean
@@ -1,6 +1,6 @@
1
module
2
set_option grind.debug true
3
-
+set_option warn.sorry false
4
/--
5
trace: [grind.offset.internalize.term] a1 ↦ #0
6
[grind.offset.internalize.term] a2 ↦ #1
@@ -274,7 +274,7 @@ trace: [grind.debug.proof] intro_with_eq (p ↔ a2 ≤ a1) (p = (a2 ≤ a1)) (¬
274
open Lean Grind in
275
set_option trace.grind.debug.proof true in
276
theorem ex1 (p : Prop) (a1 a2 a3 : Nat) : (p ↔ a2 ≤ a1) → ¬p → a2 + 3 ≤ a3 → (p ↔ a4 ≤ a3 + 2) → a1 ≤ a4 := by
277
- grind
+ grind -order
278
279
/-! Propagate `cnstr = False` tests -/
280
0 commit comments