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 9322660 commit 39609ffCopy full SHA for 39609ff
tests/pkg/module/Module/MetaImported.lean
@@ -1,6 +1,5 @@
1
module
2
3
-prelude
4
meta import Module.Basic
5
6
/-! Basic phase restriction tests. -/
0 commit comments