Initial commit
This commit is contained in:
17
lakefile.toml
Normal file
17
lakefile.toml
Normal file
@@ -0,0 +1,17 @@
|
||||
name = "aristotle"
|
||||
version = "0.1.0"
|
||||
keywords = ["math"]
|
||||
defaultTargets = ["Aristotle"]
|
||||
|
||||
[leanOptions]
|
||||
pp.unicode.fun = true # pretty-prints `fun a ↦ b`
|
||||
relaxedAutoImplicit = false
|
||||
weak.linter.mathlibStandardSet = true
|
||||
maxSynthPendingDepth = 3
|
||||
|
||||
[[require]]
|
||||
name = "mathlib"
|
||||
scope = "leanprover-community"
|
||||
|
||||
[[lean_lib]]
|
||||
name = "Aristotle"
|
||||
Reference in New Issue
Block a user