diff --git a/.gitignore b/.gitignore index 30bf676..6e543ec 100644 --- a/.gitignore +++ b/.gitignore @@ -1,4 +1,5 @@ -/build -/lake-packages/* -/_target -/leanpkg.path +# Lean +**/build +**/lake-packages/* +**/_target +**/leanpkg.path diff --git a/Bookshelf.lean b/Bookshelf.lean deleted file mode 100644 index 037efd7..0000000 --- a/Bookshelf.lean +++ /dev/null @@ -1,2 +0,0 @@ -import Bookshelf.Sequence.Arithmetic -import Bookshelf.Sequence.Geometric diff --git a/bookshelf/theorem-proving-in-lean/TheoremProvingInLean.lean b/bookshelf/theorem-proving-in-lean/TheoremProvingInLean.lean new file mode 100644 index 0000000..277ec5e --- /dev/null +++ b/bookshelf/theorem-proving-in-lean/TheoremProvingInLean.lean @@ -0,0 +1,6 @@ +import TheoremProvingInLean.Exercises2 +import TheoremProvingInLean.Exercises3 +import TheoremProvingInLean.Exercises4 +import TheoremProvingInLean.Exercises5 +import TheoremProvingInLean.Exercises7 +import TheoremProvingInLean.Exercises8 \ No newline at end of file diff --git a/exercises/theorem-proving-in-lean/exercises-2.lean b/bookshelf/theorem-proving-in-lean/TheoremProvingInLean/Exercises2.lean similarity index 100% rename from exercises/theorem-proving-in-lean/exercises-2.lean rename to bookshelf/theorem-proving-in-lean/TheoremProvingInLean/Exercises2.lean diff --git a/exercises/theorem-proving-in-lean/exercises-3.lean b/bookshelf/theorem-proving-in-lean/TheoremProvingInLean/Exercises3.lean similarity index 100% rename from exercises/theorem-proving-in-lean/exercises-3.lean rename to bookshelf/theorem-proving-in-lean/TheoremProvingInLean/Exercises3.lean diff --git a/exercises/theorem-proving-in-lean/exercises-4.lean b/bookshelf/theorem-proving-in-lean/TheoremProvingInLean/Exercises4.lean similarity index 100% rename from exercises/theorem-proving-in-lean/exercises-4.lean rename to bookshelf/theorem-proving-in-lean/TheoremProvingInLean/Exercises4.lean diff --git a/exercises/theorem-proving-in-lean/exercises-5.lean b/bookshelf/theorem-proving-in-lean/TheoremProvingInLean/Exercises5.lean similarity index 100% rename from exercises/theorem-proving-in-lean/exercises-5.lean rename to bookshelf/theorem-proving-in-lean/TheoremProvingInLean/Exercises5.lean diff --git a/exercises/theorem-proving-in-lean/exercises-7.lean b/bookshelf/theorem-proving-in-lean/TheoremProvingInLean/Exercises7.lean similarity index 100% rename from exercises/theorem-proving-in-lean/exercises-7.lean rename to bookshelf/theorem-proving-in-lean/TheoremProvingInLean/Exercises7.lean diff --git a/exercises/theorem-proving-in-lean/exercises-8.lean b/bookshelf/theorem-proving-in-lean/TheoremProvingInLean/Exercises8.lean similarity index 100% rename from exercises/theorem-proving-in-lean/exercises-8.lean rename to bookshelf/theorem-proving-in-lean/TheoremProvingInLean/Exercises8.lean diff --git a/bookshelf/theorem-proving-in-lean/lake-manifest.json b/bookshelf/theorem-proving-in-lean/lake-manifest.json new file mode 100644 index 0000000..1e31dae --- /dev/null +++ b/bookshelf/theorem-proving-in-lean/lake-manifest.json @@ -0,0 +1 @@ +{"version": 4, "packagesDir": "lake-packages", "packages": []} diff --git a/bookshelf/theorem-proving-in-lean/lakefile.lean b/bookshelf/theorem-proving-in-lean/lakefile.lean new file mode 100644 index 0000000..d989b0a --- /dev/null +++ b/bookshelf/theorem-proving-in-lean/lakefile.lean @@ -0,0 +1,7 @@ +import Lake +open Lake DSL + +package «theorem-proving-in-lean» + +@[default_target] +lean_lib «TheoremProvingInLean» diff --git a/lean-toolchain b/bookshelf/theorem-proving-in-lean/lean-toolchain similarity index 100% rename from lean-toolchain rename to bookshelf/theorem-proving-in-lean/lean-toolchain diff --git a/common/Sequence.lean b/common/Sequence.lean new file mode 100644 index 0000000..a56ac94 --- /dev/null +++ b/common/Sequence.lean @@ -0,0 +1,2 @@ +import Sequence.Arithmetic +import Sequence.Geometric \ No newline at end of file diff --git a/Bookshelf/Sequence/Arithmetic.lean b/common/Sequence/Arithmetic.lean similarity index 100% rename from Bookshelf/Sequence/Arithmetic.lean rename to common/Sequence/Arithmetic.lean diff --git a/Bookshelf/Sequence/Geometric.lean b/common/Sequence/Geometric.lean similarity index 100% rename from Bookshelf/Sequence/Geometric.lean rename to common/Sequence/Geometric.lean diff --git a/lake-manifest.json b/common/lake-manifest.json similarity index 93% rename from lake-manifest.json rename to common/lake-manifest.json index fe3e9de..d02be76 100644 --- a/lake-manifest.json +++ b/common/lake-manifest.json @@ -4,7 +4,7 @@ [{"git": {"url": "https://github.com/leanprover-community/mathlib4.git", "subDir?": null, - "rev": "065e9956724008d1059577700fd676eaf25f35d5", + "rev": "7e974fd3806866272e9f6d9e44fa04c210a21f87", "name": "mathlib", "inputRev?": null}}, {"git": diff --git a/common/lakefile.lean b/common/lakefile.lean new file mode 100644 index 0000000..b27615a --- /dev/null +++ b/common/lakefile.lean @@ -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"] +} diff --git a/common/lean-toolchain b/common/lean-toolchain new file mode 100644 index 0000000..5bf01da --- /dev/null +++ b/common/lean-toolchain @@ -0,0 +1 @@ +leanprover/lean4:nightly-2023-02-10 diff --git a/lakefile.lean b/lakefile.lean deleted file mode 100644 index 3d0e994..0000000 --- a/lakefile.lean +++ /dev/null @@ -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 -}