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 014d9ee commit 26e375aCopy full SHA for 26e375a
tests/lean/run/grind_finish_trace.lean
@@ -176,7 +176,7 @@ example (f : Int → Int) (x y : Int)
176
example (f : Int → Int) (x y : Int)
177
: 0 ≤ x → x ≤ 2 → f 0 = y → f 1 = y → f 2 = y → f x = y := by
178
grind =>
179
- -- Again, we can use `have` to goal the proof with `mbtc`
+ -- Again, we can use `have` to golf the proof with `mbtc`
180
have : x ≠ 0
181
have : x ≠ 1
182
have : x ≠ 2
0 commit comments