-
1
-
2
-
3
-
4
-
5
-
6
-
7
-
8
-
9
-
10
-
11
-
12
-
13
import Lake
open Lake DSL
package mil {
-- add package configuration options here
}
@[default_target]
lean_lib «MIL» {
-- add library configuration options here
}
require mathlib from git "https://github.com/leanprover-community/mathlib4"@"master"