pfr/lakefile.toml at master · Oliiiiver/pfr · 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
name = "PFR"
keywords = ["math", "additive-combinatorics", "information-theory"]
defaultTargets = ["PFR"]

[leanOptions]
# Pretty-prints `fun a ↦ b`
pp.unicode.fun = true
# Don't assume a typo is a new variable
autoImplicit = false
relaxedAutoImplicit = false
# Enable all mathlib linters: automatically matches what mathlib uses...
weak.linter.mathlibStandardSet = true
# ...except the header linter.
weak.linter.style.header = false
# Switch off warnings generated by `sorry`
warn.sorry = false

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

[[require]]
name = "AddCombi"
git = "https://github.com/leanprover-community/add-combi.git"
rev = "v4.31.0"

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

[[lean_lib]]
name = "PFR"