lakefile.toml

name = "BrownianMotion"
defaultTargets = ["BrownianMotion"]
lintDriver = "batteries/runLinter"

[leanOptions]
pp.unicode.fun = true
autoImplicit = false
relaxedAutoImplicit = false
weak.linter.flexible = true # no rigid tactic (e.g. `exact`) after a flexible tactic (e.g. `simp`)
# Enable all mathlib linters: automatically matches what mathlib uses.
weak.linter.mathlibStandardSet = true

[[require]]
name = "kolmogorov_extension4"
git = "https://github.com/RemyDegenne/kolmogorov_extension4"

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

[[require]]
name = "subverso"
git = "https://github.com/leanprover/subverso"

[[lean_lib]]
name = "BrownianMotion"