PrimeNumberTheoremAnd/lakefile.toml at main · AlexKontorovich/PrimeNumberTheoremAnd · GitHub

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
name = "PrimeNumberTheoremAnd"
defaultTargets = ["PrimeNumberTheoremAnd"]

[leanOptions]
pp.unicode.fun = true
pp.proofs.withType = false
autoImplicit = false
relaxedAutoImplicit = false
linter.mathlibStandardSet = true
linter.style.openClassical = false
linter.style.longLine = false
linter.style.emptyLine = false
linter.flexible = true

[[require]]
name = "LeanArchitect"
git = "https://github.com/hanwenzhu/LeanArchitect.git"
rev = "v4.28.0"

[[require]]
name = "mathlib"
git = "https://github.com/leanprover-community/mathlib4.git"
rev = "v4.28.0"

[[require]]
name = "checkdecls"
git = "https://github.com/PatrickMassot/checkdecls.git"

[[require]]
name = "leancert"
git = "https://github.com/alerad/leancert"
rev = "v4.28.1"

[[require]]
name = "PrimeCert"
git = "https://github.com/b-mehta/PrimeCert"
rev = "v4.28.0"

[[lean_lib]]
name = "PrimeNumberTheoremAnd"