We read every piece of feedback, and take your input very seriously.
To see all available qualifiers, see our documentation.
1 parent 316993c commit 4ffe82eCopy full SHA for 4ffe82e
README.md
@@ -1,8 +1,14 @@
1
# lean-project
2
3
```bash
4
+$ lake exe mk_all
5
+No update necessary
6
$ lake build
-Build completed successfully (579 jobs).
7
+ℹ [496/498] Replayed Project.Example
8
+info: Project/Example.lean:29:0: import Mathlib.Data.Nat.Factorial.Basic
9
+import Mathlib.Data.Nat.Prime.Defs
10
+info: Project/Example.lean:29:0: `#`-commands, such as '#min_imports', are not allowed in 'Mathlib' [linter.hashCommand]
11
+Build completed successfully (498 jobs).
12
```
13
14
## How to use
0 commit comments