name = "NewProject" defaultTargets = ["NewProject"] [leanOptions] pp.unicode.fun = true autoImplicit = false relaxedAutoImplicit = false [[require]] name = "mathlib" git = "https://github.com/leanprover-community/mathlib4.git" [[require]] name = "checkdecls" git = "https://github.com/PatrickMassot/checkdecls.git" [[require]] name = "«doc-gen4»" git = "https://github.com/leanprover/doc-gen4" rev = "main" [[lean_lib]] name = "NewProject"