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 7a0fc2f commit d524bc1Copy full SHA for d524bc1
tests/lean/run/grind_offset.lean
@@ -77,8 +77,6 @@ trace: [grind.assert] foo (c + 1) = a
77
[grind.assert] ¬a = g (foo b)
78
[grind.ematch.instance] foo.eq_3: foo b.succ.succ = g (foo b)
79
[grind.assert] foo (b + 2) = g (foo b)
80
-[grind.assert] c + 1 = b + 2
81
-[grind.assert] ¬c + 1 = b + 2
82
-/
83
#guard_msgs (trace) in
84
example : foo (c + 1) = a → c = b + 1 → a = g (foo b) := by
0 commit comments