Break books into separate Lean projects.

finite-set-exercises
Joshua Potter 2023-02-20 13:26:18 -07:00
parent 827229a927
commit e607a0efb0
19 changed files with 35 additions and 21 deletions

9
.gitignore vendored
View File

@ -1,4 +1,5 @@
/build
/lake-packages/*
/_target
/leanpkg.path
# Lean
**/build
**/lake-packages/*
**/_target
**/leanpkg.path

View File

@ -1,2 +0,0 @@
import Bookshelf.Sequence.Arithmetic
import Bookshelf.Sequence.Geometric

View File

@ -0,0 +1,6 @@
import TheoremProvingInLean.Exercises2
import TheoremProvingInLean.Exercises3
import TheoremProvingInLean.Exercises4
import TheoremProvingInLean.Exercises5
import TheoremProvingInLean.Exercises7
import TheoremProvingInLean.Exercises8

View File

@ -0,0 +1 @@
{"version": 4, "packagesDir": "lake-packages", "packages": []}

View File

@ -0,0 +1,7 @@
import Lake
open Lake DSL
package «theorem-proving-in-lean»
@[default_target]
lean_lib «TheoremProvingInLean»

2
common/Sequence.lean Normal file
View File

@ -0,0 +1,2 @@
import Sequence.Arithmetic
import Sequence.Geometric

View File

@ -4,7 +4,7 @@
[{"git":
{"url": "https://github.com/leanprover-community/mathlib4.git",
"subDir?": null,
"rev": "065e9956724008d1059577700fd676eaf25f35d5",
"rev": "7e974fd3806866272e9f6d9e44fa04c210a21f87",
"name": "mathlib",
"inputRev?": null}},
{"git":

12
common/lakefile.lean Normal file
View File

@ -0,0 +1,12 @@
import Lake
open Lake DSL
require mathlib from git
"https://github.com/leanprover-community/mathlib4.git"
package «Common»
@[default_target]
lean_lib «Common» {
roots := #["Sequence"]
}

1
common/lean-toolchain Normal file
View File

@ -0,0 +1 @@
leanprover/lean4:nightly-2023-02-10

View File

@ -1,14 +0,0 @@
import Lake
open Lake DSL
require mathlib from git
"https://github.com/leanprover-community/mathlib4.git"
package «bookshelf» {
-- add package configuration options here
}
@[default_target]
lean_lib «Bookshelf» {
-- add library configuration options here
}