-
Notifications
You must be signed in to change notification settings - Fork 1
/
Copy pathlakefile.lean
40 lines (24 loc) · 1.16 KB
/
lakefile.lean
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
import Lake
open Lake DSL
def moreServerArgs := #[
"-Dpp.unicode.fun=true", -- pretty-prints `fun a ↦ b`
"-DautoImplicit=false",
"-DrelaxedAutoImplicit=false"
]
-- These settings only apply during `lake build`, but not in VSCode editor.
def moreLeanArgs := moreServerArgs
-- moreServerArgs
package «leanCourse» where
moreServerArgs := moreServerArgs
require mathlib from git
"https://github.com/leanprover-community/mathlib4.git"@"v4.2.0"
require Paperproof from git "https://github.com/Paper-Proof/paperproof.git"@"main"/"lean"
require proofwidgets from git "https://github.com/leanprover-community/ProofWidgets4"@"v0.0.3"
require MATH681CourseProject from git "https://github.com/davidowe/MATH681CourseProject.git"
-- require MIL from git "https://github.com/avigad/mathematics_in_lean_source.git"
require LADR3 from git "https://github.com/martincmartin/linear_algebra_done_right.git"
-- require FM2024 from git "https://github.com/ImperialCollegeLondon/formalising-mathematics-2024.git"
-- require Duper from git "https://github.com/leanprover-community/duper.git" @ "v0.0.5"
@[default_target]
lean_lib «LeanCourse» where
moreLeanArgs := moreLeanArgs