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 7856fdf commit a81701fCopy full SHA for a81701f
tests/lean/run/grind_finish_trace.lean
@@ -45,7 +45,7 @@ example {α : Type} (op : α → α → α) [Std.Associative op] [Std.Commutativ
45
/--
46
info: Try this:
47
[apply] ⏎
48
- instantiate only [= Array.getElem_set, = Array.size_set]
+ instantiate only [= Array.getElem_set]
49
instantiate only [= Array.getElem_set]
50
-/
51
#guard_msgs in
0 commit comments