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 c5f8ac9 commit b0e8728Copy full SHA for b0e8728
Mathlib/Tactic/Linter/PrivateModule.lean
@@ -1,3 +1,8 @@
1
+/-
2
+Copyright (c) 2025 Thomas R. Murrills. All rights reserved.
3
+Released under Apache 2.0 license as described in the file LICENSE.
4
+Authors: Thomas R. Murrills
5
+-/
6
module
7
8
public import Mathlib.Init
0 commit comments