name = "GWchap5"
defaultTargets = ["GWchap5"]

[leanOptions]
pp.unicode.fun = true
autoImplicit = false
relaxedAutoImplicit = false

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


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

[[require]]
name = "«doc-gen4»"
git = "https://github.com/leanprover/doc-gen4"
rev = "v4.24.0"

# [[require]]
# name = "LeanCopilot"
# git = "https://github.com/lean-dojo/LeanCopilot.git"
# rev = "v4.21.0" # Use the version matching your lean-toolchain file


[[lean_lib]]
name = "GWchap5"
# moreLinkArgs = ["-L./.lake/packages/LeanCopilot/.lake/build/lib", "-lctranslate2"]