We read every piece of feedback, and take your input very seriously.
To see all available qualifiers, see our documentation.
1 parent da0c70b commit 14b70bcCopy full SHA for 14b70bc
Mathlib/Tactic/TacticAnalysis/Declarations.lean
@@ -3,6 +3,7 @@ Copyright (c) 2025 Lean FRO, LLC. All rights reserved.
3
Released under Apache 2.0 license as described in the file LICENSE.
4
Authors: Anne Baanen, Edward van de Meent
5
-/
6
+module
7
8
public meta import Mathlib.Tactic.TacticAnalysis
9
public meta import Mathlib.Tactic.ExtractGoal
0 commit comments