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 5326530 commit e29faaaCopy full SHA for e29faaa
src/Lean/Meta/Tactic/Try/Collect.lean
@@ -7,8 +7,6 @@ module
7
prelude
8
public import Init.Try
9
public import Lean.Meta.Tactic.LibrarySearch
10
-public import Lean.Meta.Tactic.Grind.Cases
11
-public import Lean.Meta.Tactic.Grind.EMatchTheorem
12
public import Lean.Meta.Tactic.FunIndCollect
13
import Lean.Meta.Eqns
14
public section
0 commit comments