lean/MathlibExamples/lakefile.toml

name = "test0"
version = "0.1.0"
keywords = ["math"]
defaultTargets = ["MathlibExamples"]

[leanOptions]
pp.unicode.fun = true # pretty-prints `fun a ↦ b`
autoImplicit = false
relaxedAutoImplicit = false
weak.linter.mathlibStandardSet = true
maxSynthPendingDepth = 3

[[require]]
name = "mathlib"
scope = "leanprover-community"
rev = "v4.24.0"

[[lean_lib]]
name = "MathlibExamples"