diff --git a/.gitignore b/.gitignore index 39d8ebd..7e41fc2 100644 --- a/.gitignore +++ b/.gitignore @@ -1,8 +1,8 @@ # Lean -*/build -*/lake-packages -*/_target -*/leanpkg.path +build +lake-packages +_target +leanpkg.path # TeX *.aux diff --git a/shared/Bookshelf.lean b/Bookshelf.lean similarity index 65% rename from shared/Bookshelf.lean rename to Bookshelf.lean index e9c99a8..09cf26e 100644 --- a/shared/Bookshelf.lean +++ b/Bookshelf.lean @@ -1,3 +1,3 @@ import Bookshelf.List import Bookshelf.Real -import Bookshelf.Tuple +import Bookshelf.Tuple \ No newline at end of file diff --git a/shared/Bookshelf/List.lean b/Bookshelf/List.lean similarity index 100% rename from shared/Bookshelf/List.lean rename to Bookshelf/List.lean diff --git a/shared/Bookshelf/List/Basic.lean b/Bookshelf/List/Basic.lean similarity index 100% rename from shared/Bookshelf/List/Basic.lean rename to Bookshelf/List/Basic.lean diff --git a/shared/Bookshelf/Real.lean b/Bookshelf/Real.lean similarity index 100% rename from shared/Bookshelf/Real.lean rename to Bookshelf/Real.lean diff --git a/shared/Bookshelf/Real/Basic.lean b/Bookshelf/Real/Basic.lean similarity index 100% rename from shared/Bookshelf/Real/Basic.lean rename to Bookshelf/Real/Basic.lean diff --git a/shared/Bookshelf/Real/Rational.lean b/Bookshelf/Real/Rational.lean similarity index 100% rename from shared/Bookshelf/Real/Rational.lean rename to Bookshelf/Real/Rational.lean diff --git a/shared/Bookshelf/Real/Sequence.lean b/Bookshelf/Real/Sequence.lean similarity index 100% rename from shared/Bookshelf/Real/Sequence.lean rename to Bookshelf/Real/Sequence.lean diff --git a/shared/Bookshelf/Real/Sequence.tex b/Bookshelf/Real/Sequence.tex similarity index 100% rename from shared/Bookshelf/Real/Sequence.tex rename to Bookshelf/Real/Sequence.tex diff --git a/shared/Bookshelf/Real/Sequence/Arithmetic.lean b/Bookshelf/Real/Sequence/Arithmetic.lean similarity index 100% rename from shared/Bookshelf/Real/Sequence/Arithmetic.lean rename to Bookshelf/Real/Sequence/Arithmetic.lean diff --git a/shared/Bookshelf/Real/Sequence/Geometric.lean b/Bookshelf/Real/Sequence/Geometric.lean similarity index 100% rename from shared/Bookshelf/Real/Sequence/Geometric.lean rename to Bookshelf/Real/Sequence/Geometric.lean diff --git a/shared/Bookshelf/Real/Set.lean b/Bookshelf/Real/Set.lean similarity index 100% rename from shared/Bookshelf/Real/Set.lean rename to Bookshelf/Real/Set.lean diff --git a/shared/Bookshelf/Real/Set/Basic.lean b/Bookshelf/Real/Set/Basic.lean similarity index 100% rename from shared/Bookshelf/Real/Set/Basic.lean rename to Bookshelf/Real/Set/Basic.lean diff --git a/shared/Bookshelf/Real/Set/Interval.lean b/Bookshelf/Real/Set/Interval.lean similarity index 100% rename from shared/Bookshelf/Real/Set/Interval.lean rename to Bookshelf/Real/Set/Interval.lean diff --git a/shared/Bookshelf/Tuple.lean b/Bookshelf/Tuple.lean similarity index 100% rename from shared/Bookshelf/Tuple.lean rename to Bookshelf/Tuple.lean diff --git a/FirstCourseAbstractAlgebra.lean b/FirstCourseAbstractAlgebra.lean new file mode 100644 index 0000000..17778be --- /dev/null +++ b/FirstCourseAbstractAlgebra.lean @@ -0,0 +1 @@ +import FirstCourseAbstractAlgebra.Fraleigh \ No newline at end of file diff --git a/FirstCourseAbstractAlgebra/Fraleigh.lean b/FirstCourseAbstractAlgebra/Fraleigh.lean new file mode 100644 index 0000000..05d27be --- /dev/null +++ b/FirstCourseAbstractAlgebra/Fraleigh.lean @@ -0,0 +1 @@ +import FirstCourseAbstractAlgebra.Fraleigh.Chapter1 diff --git a/first-course-abstract-algebra/Fraleigh/Chapter1.lean b/FirstCourseAbstractAlgebra/Fraleigh/Chapter1.lean similarity index 100% rename from first-course-abstract-algebra/Fraleigh/Chapter1.lean rename to FirstCourseAbstractAlgebra/Fraleigh/Chapter1.lean diff --git a/first-course-abstract-algebra/README.md b/FirstCourseAbstractAlgebra/README.md similarity index 100% rename from first-course-abstract-algebra/README.md rename to FirstCourseAbstractAlgebra/README.md diff --git a/MathematicalIntroductionLogic.lean b/MathematicalIntroductionLogic.lean new file mode 100644 index 0000000..de93443 --- /dev/null +++ b/MathematicalIntroductionLogic.lean @@ -0,0 +1 @@ +import MathematicalIntroductionLogic.Enderton \ No newline at end of file diff --git a/MathematicalIntroductionLogic/Enderton.lean b/MathematicalIntroductionLogic/Enderton.lean new file mode 100644 index 0000000..3a2ee26 --- /dev/null +++ b/MathematicalIntroductionLogic/Enderton.lean @@ -0,0 +1 @@ +import MathematicalIntroductionLogic.Enderton.Chapter0 diff --git a/mathematical-introduction-logic/Enderton/Chapter0.lean b/MathematicalIntroductionLogic/Enderton/Chapter0.lean similarity index 100% rename from mathematical-introduction-logic/Enderton/Chapter0.lean rename to MathematicalIntroductionLogic/Enderton/Chapter0.lean diff --git a/mathematical-introduction-logic/Enderton/Chapter0.tex b/MathematicalIntroductionLogic/Enderton/Chapter0.tex similarity index 91% rename from mathematical-introduction-logic/Enderton/Chapter0.tex rename to MathematicalIntroductionLogic/Enderton/Chapter0.tex index 220e82e..24fbaf9 100644 --- a/mathematical-introduction-logic/Enderton/Chapter0.tex +++ b/MathematicalIntroductionLogic/Enderton/Chapter0.tex @@ -1,6 +1,6 @@ \documentclass{article} -\input{../../shared/preamble} +\input{../../preamble} \begin{document} diff --git a/mathematical-introduction-logic/README.md b/MathematicalIntroductionLogic/README.md similarity index 100% rename from mathematical-introduction-logic/README.md rename to MathematicalIntroductionLogic/README.md diff --git a/MockMockingbird.lean b/MockMockingbird.lean new file mode 100644 index 0000000..232c8ff --- /dev/null +++ b/MockMockingbird.lean @@ -0,0 +1 @@ +import MockMockingbird.Smullyan \ No newline at end of file diff --git a/mock-mockingbird/Smullyan.lean b/MockMockingbird/Smullyan.lean similarity index 100% rename from mock-mockingbird/Smullyan.lean rename to MockMockingbird/Smullyan.lean diff --git a/mock-mockingbird/Smullyan/Aviary.lean b/MockMockingbird/Smullyan/Aviary.lean similarity index 100% rename from mock-mockingbird/Smullyan/Aviary.lean rename to MockMockingbird/Smullyan/Aviary.lean diff --git a/mock-mockingbird/Smullyan/Aviary.tex b/MockMockingbird/Smullyan/Aviary.tex similarity index 98% rename from mock-mockingbird/Smullyan/Aviary.tex rename to MockMockingbird/Smullyan/Aviary.tex index 7ff81c7..011478e 100644 --- a/mock-mockingbird/Smullyan/Aviary.tex +++ b/MockMockingbird/Smullyan/Aviary.tex @@ -1,6 +1,6 @@ \documentclass{article} -\input{../../shared/preamble} +\input{../../preamble} \begin{document} diff --git a/OneVariableCalculus.lean b/OneVariableCalculus.lean new file mode 100644 index 0000000..f1f7109 --- /dev/null +++ b/OneVariableCalculus.lean @@ -0,0 +1 @@ +import OneVariableCalculus.Apostol \ No newline at end of file diff --git a/OneVariableCalculus/Apostol.lean b/OneVariableCalculus/Apostol.lean new file mode 100644 index 0000000..595e783 --- /dev/null +++ b/OneVariableCalculus/Apostol.lean @@ -0,0 +1,3 @@ +import OneVariableCalculus.Apostol.Chapters +import OneVariableCalculus.Apostol.Exercises +import OneVariableCalculus.Apostol.Real \ No newline at end of file diff --git a/OneVariableCalculus/Apostol/Chapters.lean b/OneVariableCalculus/Apostol/Chapters.lean new file mode 100644 index 0000000..755a900 --- /dev/null +++ b/OneVariableCalculus/Apostol/Chapters.lean @@ -0,0 +1 @@ +import OneVariableCalculus.Apostol.Chapters.Chapter_I_3 \ No newline at end of file diff --git a/one-variable-calculus/Apostol/Chapters/Chapter_I_3.lean b/OneVariableCalculus/Apostol/Chapters/Chapter_I_3.lean similarity index 100% rename from one-variable-calculus/Apostol/Chapters/Chapter_I_3.lean rename to OneVariableCalculus/Apostol/Chapters/Chapter_I_3.lean diff --git a/one-variable-calculus/Apostol/Chapters/Chapter_I_3.tex b/OneVariableCalculus/Apostol/Chapters/Chapter_I_3.tex similarity index 99% rename from one-variable-calculus/Apostol/Chapters/Chapter_I_3.tex rename to OneVariableCalculus/Apostol/Chapters/Chapter_I_3.tex index babbc75..0892ac0 100644 --- a/one-variable-calculus/Apostol/Chapters/Chapter_I_3.tex +++ b/OneVariableCalculus/Apostol/Chapters/Chapter_I_3.tex @@ -1,7 +1,7 @@ \documentclass{article} \usepackage[shortlabels]{enumitem} -\input{../../shared/preamble} +\input{../../../preamble} \begin{document} diff --git a/OneVariableCalculus/Apostol/Exercises.lean b/OneVariableCalculus/Apostol/Exercises.lean new file mode 100644 index 0000000..d918be5 --- /dev/null +++ b/OneVariableCalculus/Apostol/Exercises.lean @@ -0,0 +1 @@ +import OneVariableCalculus.Apostol.Exercises.Exercises_I_3_12 \ No newline at end of file diff --git a/one-variable-calculus/Apostol/Exercises/Exercises_1_7.lean b/OneVariableCalculus/Apostol/Exercises/Exercises_1_7.lean similarity index 100% rename from one-variable-calculus/Apostol/Exercises/Exercises_1_7.lean rename to OneVariableCalculus/Apostol/Exercises/Exercises_1_7.lean diff --git a/one-variable-calculus/Apostol/Exercises/Exercises_I_3_12.lean b/OneVariableCalculus/Apostol/Exercises/Exercises_I_3_12.lean similarity index 99% rename from one-variable-calculus/Apostol/Exercises/Exercises_I_3_12.lean rename to OneVariableCalculus/Apostol/Exercises/Exercises_I_3_12.lean index 286397a..1e0abe3 100644 --- a/one-variable-calculus/Apostol/Exercises/Exercises_I_3_12.lean +++ b/OneVariableCalculus/Apostol/Exercises/Exercises_I_3_12.lean @@ -9,8 +9,8 @@ import Mathlib.Data.Real.Basic import Mathlib.Data.Real.Sqrt import Mathlib.Tactic.LibrarySearch -import Apostol.Chapters.Chapter_I_3 import Bookshelf.Real.Rational +import OneVariableCalculus.Apostol.Chapters.Chapter_I_3 -- ======================================== -- Exercise 1 diff --git a/OneVariableCalculus/Apostol/Real.lean b/OneVariableCalculus/Apostol/Real.lean new file mode 100644 index 0000000..3dc33c5 --- /dev/null +++ b/OneVariableCalculus/Apostol/Real.lean @@ -0,0 +1,3 @@ +import OneVariableCalculus.Apostol.Real.Function +import OneVariableCalculus.Apostol.Real.Geometry +import OneVariableCalculus.Apostol.Real.Set \ No newline at end of file diff --git a/OneVariableCalculus/Apostol/Real/Function.lean b/OneVariableCalculus/Apostol/Real/Function.lean new file mode 100644 index 0000000..fbf59d1 --- /dev/null +++ b/OneVariableCalculus/Apostol/Real/Function.lean @@ -0,0 +1 @@ +import OneVariableCalculus.Apostol.Real.Function.Step \ No newline at end of file diff --git a/one-variable-calculus/Apostol/Real/Function/Step.lean b/OneVariableCalculus/Apostol/Real/Function/Step.lean similarity index 92% rename from one-variable-calculus/Apostol/Real/Function/Step.lean rename to OneVariableCalculus/Apostol/Real/Function/Step.lean index abf9e65..1076e3f 100644 --- a/one-variable-calculus/Apostol/Real/Function/Step.lean +++ b/OneVariableCalculus/Apostol/Real/Function/Step.lean @@ -1,8 +1,8 @@ import Mathlib.Data.Fin.Basic import Mathlib.Tactic.NormNum -import Apostol.Real.Set.Partition import Bookshelf.Real.Basic +import OneVariableCalculus.Apostol.Real.Set.Partition namespace Real.Function diff --git a/OneVariableCalculus/Apostol/Real/Geometry.lean b/OneVariableCalculus/Apostol/Real/Geometry.lean new file mode 100644 index 0000000..f93a06b --- /dev/null +++ b/OneVariableCalculus/Apostol/Real/Geometry.lean @@ -0,0 +1,3 @@ +import OneVariableCalculus.Apostol.Real.Geometry.Area +import OneVariableCalculus.Apostol.Real.Geometry.Basic +import OneVariableCalculus.Apostol.Real.Geometry.Rectangle \ No newline at end of file diff --git a/one-variable-calculus/Apostol/Real/Geometry/Area.lean b/OneVariableCalculus/Apostol/Real/Geometry/Area.lean similarity index 97% rename from one-variable-calculus/Apostol/Real/Geometry/Area.lean rename to OneVariableCalculus/Apostol/Real/Geometry/Area.lean index 8ac3183..586f242 100644 --- a/one-variable-calculus/Apostol/Real/Geometry/Area.lean +++ b/OneVariableCalculus/Apostol/Real/Geometry/Area.lean @@ -3,8 +3,8 @@ Chapter 1.6 The concept of area as a set function -/ -import Apostol.Real.Function.Step -import Apostol.Real.Geometry.Rectangle +import OneVariableCalculus.Apostol.Real.Function.Step +import OneVariableCalculus.Apostol.Real.Geometry.Rectangle namespace Real.Geometry.Area diff --git a/one-variable-calculus/Apostol/Real/Geometry/Basic.lean b/OneVariableCalculus/Apostol/Real/Geometry/Basic.lean similarity index 100% rename from one-variable-calculus/Apostol/Real/Geometry/Basic.lean rename to OneVariableCalculus/Apostol/Real/Geometry/Basic.lean diff --git a/one-variable-calculus/Apostol/Real/Geometry/Rectangle.lean b/OneVariableCalculus/Apostol/Real/Geometry/Rectangle.lean similarity index 97% rename from one-variable-calculus/Apostol/Real/Geometry/Rectangle.lean rename to OneVariableCalculus/Apostol/Real/Geometry/Rectangle.lean index aec4728..00357ba 100644 --- a/one-variable-calculus/Apostol/Real/Geometry/Rectangle.lean +++ b/OneVariableCalculus/Apostol/Real/Geometry/Rectangle.lean @@ -1,4 +1,4 @@ -import Apostol.Real.Geometry.Basic +import OneVariableCalculus.Apostol.Real.Geometry.Basic namespace Real diff --git a/OneVariableCalculus/Apostol/Real/Set.lean b/OneVariableCalculus/Apostol/Real/Set.lean new file mode 100644 index 0000000..1ae75b6 --- /dev/null +++ b/OneVariableCalculus/Apostol/Real/Set.lean @@ -0,0 +1 @@ +import OneVariableCalculus.Apostol.Real.Set.Partition \ No newline at end of file diff --git a/one-variable-calculus/Apostol/Real/Set/Partition.lean b/OneVariableCalculus/Apostol/Real/Set/Partition.lean similarity index 100% rename from one-variable-calculus/Apostol/Real/Set/Partition.lean rename to OneVariableCalculus/Apostol/Real/Set/Partition.lean diff --git a/one-variable-calculus/README.md b/OneVariableCalculus/README.md similarity index 100% rename from one-variable-calculus/README.md rename to OneVariableCalculus/README.md diff --git a/TheoremProvingInLean.lean b/TheoremProvingInLean.lean new file mode 100644 index 0000000..197a0a6 --- /dev/null +++ b/TheoremProvingInLean.lean @@ -0,0 +1 @@ +import TheoremProvingInLean.Avigad \ No newline at end of file diff --git a/TheoremProvingInLean/Avigad.lean b/TheoremProvingInLean/Avigad.lean new file mode 100644 index 0000000..7b091f1 --- /dev/null +++ b/TheoremProvingInLean/Avigad.lean @@ -0,0 +1,6 @@ +import TheoremProvingInLean.Avigad.Chapter2 +import TheoremProvingInLean.Avigad.Chapter3 +import TheoremProvingInLean.Avigad.Chapter4 +import TheoremProvingInLean.Avigad.Chapter5 +import TheoremProvingInLean.Avigad.Chapter7 +import TheoremProvingInLean.Avigad.Chapter8 diff --git a/theorem-proving-in-lean/Avigad/Chapter2.lean b/TheoremProvingInLean/Avigad/Chapter2.lean similarity index 100% rename from theorem-proving-in-lean/Avigad/Chapter2.lean rename to TheoremProvingInLean/Avigad/Chapter2.lean diff --git a/theorem-proving-in-lean/Avigad/Chapter3.lean b/TheoremProvingInLean/Avigad/Chapter3.lean similarity index 100% rename from theorem-proving-in-lean/Avigad/Chapter3.lean rename to TheoremProvingInLean/Avigad/Chapter3.lean diff --git a/theorem-proving-in-lean/Avigad/Chapter4.lean b/TheoremProvingInLean/Avigad/Chapter4.lean similarity index 100% rename from theorem-proving-in-lean/Avigad/Chapter4.lean rename to TheoremProvingInLean/Avigad/Chapter4.lean diff --git a/theorem-proving-in-lean/Avigad/Chapter5.lean b/TheoremProvingInLean/Avigad/Chapter5.lean similarity index 100% rename from theorem-proving-in-lean/Avigad/Chapter5.lean rename to TheoremProvingInLean/Avigad/Chapter5.lean diff --git a/theorem-proving-in-lean/Avigad/Chapter7.lean b/TheoremProvingInLean/Avigad/Chapter7.lean similarity index 100% rename from theorem-proving-in-lean/Avigad/Chapter7.lean rename to TheoremProvingInLean/Avigad/Chapter7.lean diff --git a/theorem-proving-in-lean/Avigad/Chapter8.lean b/TheoremProvingInLean/Avigad/Chapter8.lean similarity index 100% rename from theorem-proving-in-lean/Avigad/Chapter8.lean rename to TheoremProvingInLean/Avigad/Chapter8.lean diff --git a/theorem-proving-in-lean/README.md b/TheoremProvingInLean/README.md similarity index 100% rename from theorem-proving-in-lean/README.md rename to TheoremProvingInLean/README.md diff --git a/first-course-abstract-algebra/Fraleigh.lean b/first-course-abstract-algebra/Fraleigh.lean deleted file mode 100644 index d3e8abf..0000000 --- a/first-course-abstract-algebra/Fraleigh.lean +++ /dev/null @@ -1 +0,0 @@ -import Fraleigh.Chapter1 diff --git a/first-course-abstract-algebra/lake-manifest.json b/first-course-abstract-algebra/lake-manifest.json deleted file mode 100644 index b594809..0000000 --- a/first-course-abstract-algebra/lake-manifest.json +++ /dev/null @@ -1,28 +0,0 @@ -{"version": 4, - "packagesDir": "lake-packages", - "packages": - [{"path": {"name": "Bookshelf", "dir": "./../shared"}}, - {"git": - {"url": "https://github.com/leanprover-community/mathlib4.git", - "subDir?": null, - "rev": "0107c50abf149a48b5b9ad08a0b2a2093bcb567a", - "name": "mathlib", - "inputRev?": "0107c50abf149a48b5b9ad08a0b2a2093bcb567a"}}, - {"git": - {"url": "https://github.com/gebner/quote4", - "subDir?": null, - "rev": "7ae096b232087096ff0243a2b70d32720d2621ae", - "name": "Qq", - "inputRev?": "master"}}, - {"git": - {"url": "https://github.com/JLimperg/aesop", - "subDir?": null, - "rev": "071464ac36e339afb7a87640aa1f8121f707a59a", - "name": "aesop", - "inputRev?": "master"}}, - {"git": - {"url": "https://github.com/leanprover/std4", - "subDir?": null, - "rev": "5507f9d8409f93b984ce04eccf4914d534e6fca2", - "name": "std", - "inputRev?": "main"}}]} diff --git a/first-course-abstract-algebra/lakefile.lean b/first-course-abstract-algebra/lakefile.lean deleted file mode 100644 index b09cff8..0000000 --- a/first-course-abstract-algebra/lakefile.lean +++ /dev/null @@ -1,12 +0,0 @@ -import Lake -open Lake DSL - -package «first-course-abstract-algebra» - -require Bookshelf from "../shared" -require mathlib from git - "https://github.com/leanprover-community/mathlib4.git" @ - "0107c50abf149a48b5b9ad08a0b2a2093bcb567a" - -@[default_target] -lean_lib «fraleigh» diff --git a/shared/lake-manifest.json b/lake-manifest.json similarity index 100% rename from shared/lake-manifest.json rename to lake-manifest.json diff --git a/lakefile.lean b/lakefile.lean new file mode 100644 index 0000000..9f8afd4 --- /dev/null +++ b/lakefile.lean @@ -0,0 +1,20 @@ +import Lake +open Lake DSL + +package «bookshelf» + +require mathlib from git + "https://github.com/leanprover-community/mathlib4.git" @ + "0107c50abf149a48b5b9ad08a0b2a2093bcb567a" + +@[default_target] +lean_lib «Bookshelf» { + roots := #[ + `Bookshelf, + `FirstCourseAbstractAlgebra, + `MathematicalIntroductionLogic, + `MockMockingbird, + `OneVariableCalculus, + `TheoremProvingInLean + ] +} diff --git a/first-course-abstract-algebra/lean-toolchain b/lean-toolchain similarity index 100% rename from first-course-abstract-algebra/lean-toolchain rename to lean-toolchain diff --git a/mathematical-introduction-logic/Enderton.lean b/mathematical-introduction-logic/Enderton.lean deleted file mode 100644 index c336653..0000000 --- a/mathematical-introduction-logic/Enderton.lean +++ /dev/null @@ -1 +0,0 @@ -import Enderton.Chapter0 diff --git a/mathematical-introduction-logic/lake-manifest.json b/mathematical-introduction-logic/lake-manifest.json deleted file mode 100644 index b594809..0000000 --- a/mathematical-introduction-logic/lake-manifest.json +++ /dev/null @@ -1,28 +0,0 @@ -{"version": 4, - "packagesDir": "lake-packages", - "packages": - [{"path": {"name": "Bookshelf", "dir": "./../shared"}}, - {"git": - {"url": "https://github.com/leanprover-community/mathlib4.git", - "subDir?": null, - "rev": "0107c50abf149a48b5b9ad08a0b2a2093bcb567a", - "name": "mathlib", - "inputRev?": "0107c50abf149a48b5b9ad08a0b2a2093bcb567a"}}, - {"git": - {"url": "https://github.com/gebner/quote4", - "subDir?": null, - "rev": "7ae096b232087096ff0243a2b70d32720d2621ae", - "name": "Qq", - "inputRev?": "master"}}, - {"git": - {"url": "https://github.com/JLimperg/aesop", - "subDir?": null, - "rev": "071464ac36e339afb7a87640aa1f8121f707a59a", - "name": "aesop", - "inputRev?": "master"}}, - {"git": - {"url": "https://github.com/leanprover/std4", - "subDir?": null, - "rev": "5507f9d8409f93b984ce04eccf4914d534e6fca2", - "name": "std", - "inputRev?": "main"}}]} diff --git a/mathematical-introduction-logic/lakefile.lean b/mathematical-introduction-logic/lakefile.lean deleted file mode 100644 index 3848b97..0000000 --- a/mathematical-introduction-logic/lakefile.lean +++ /dev/null @@ -1,9 +0,0 @@ -import Lake -open Lake DSL - -package «mathematical-introduction-logic» - -require Bookshelf from "../shared" - -@[default_target] -lean_lib «enderton» diff --git a/mathematical-introduction-logic/lean-toolchain b/mathematical-introduction-logic/lean-toolchain deleted file mode 100644 index d30699b..0000000 --- a/mathematical-introduction-logic/lean-toolchain +++ /dev/null @@ -1 +0,0 @@ -leanprover/lean4:nightly-2023-04-02 diff --git a/mock-mockingbird/lakefile.lean b/mock-mockingbird/lakefile.lean deleted file mode 100644 index fdbb0cf..0000000 --- a/mock-mockingbird/lakefile.lean +++ /dev/null @@ -1,7 +0,0 @@ -import Lake -open Lake DSL - -package «mock-mockingbird» - -@[default_target] -lean_lib «Smullyan» \ No newline at end of file diff --git a/mock-mockingbird/lean-toolchain b/mock-mockingbird/lean-toolchain deleted file mode 100644 index d30699b..0000000 --- a/mock-mockingbird/lean-toolchain +++ /dev/null @@ -1 +0,0 @@ -leanprover/lean4:nightly-2023-04-02 diff --git a/one-variable-calculus/Apostol.lean b/one-variable-calculus/Apostol.lean deleted file mode 100644 index d500f82..0000000 --- a/one-variable-calculus/Apostol.lean +++ /dev/null @@ -1,3 +0,0 @@ -import Apostol.Chapters -import Apostol.Exercises -import Apostol.Real \ No newline at end of file diff --git a/one-variable-calculus/Apostol/Chapters.lean b/one-variable-calculus/Apostol/Chapters.lean deleted file mode 100644 index b132282..0000000 --- a/one-variable-calculus/Apostol/Chapters.lean +++ /dev/null @@ -1 +0,0 @@ -import Apostol.Chapters.Chapter_I_3 \ No newline at end of file diff --git a/one-variable-calculus/Apostol/Exercises.lean b/one-variable-calculus/Apostol/Exercises.lean deleted file mode 100644 index e0f7a10..0000000 --- a/one-variable-calculus/Apostol/Exercises.lean +++ /dev/null @@ -1 +0,0 @@ -import Apostol.Exercises.Exercises_I_3_12 \ No newline at end of file diff --git a/one-variable-calculus/Apostol/Real.lean b/one-variable-calculus/Apostol/Real.lean deleted file mode 100644 index 90f9546..0000000 --- a/one-variable-calculus/Apostol/Real.lean +++ /dev/null @@ -1,3 +0,0 @@ -import Apostol.Real.Function -import Apostol.Real.Geometry -import Apostol.Real.Set \ No newline at end of file diff --git a/one-variable-calculus/Apostol/Real/Function.lean b/one-variable-calculus/Apostol/Real/Function.lean deleted file mode 100644 index 10a38e7..0000000 --- a/one-variable-calculus/Apostol/Real/Function.lean +++ /dev/null @@ -1 +0,0 @@ -import Apostol.Real.Function.Step \ No newline at end of file diff --git a/one-variable-calculus/Apostol/Real/Geometry.lean b/one-variable-calculus/Apostol/Real/Geometry.lean deleted file mode 100644 index 20bd0f7..0000000 --- a/one-variable-calculus/Apostol/Real/Geometry.lean +++ /dev/null @@ -1,3 +0,0 @@ -import Apostol.Real.Geometry.Area -import Apostol.Real.Geometry.Basic -import Apostol.Real.Geometry.Rectangle \ No newline at end of file diff --git a/one-variable-calculus/Apostol/Real/Set.lean b/one-variable-calculus/Apostol/Real/Set.lean deleted file mode 100644 index cb51552..0000000 --- a/one-variable-calculus/Apostol/Real/Set.lean +++ /dev/null @@ -1 +0,0 @@ -import Apostol.Real.Set.Partition \ No newline at end of file diff --git a/one-variable-calculus/lake-manifest.json b/one-variable-calculus/lake-manifest.json deleted file mode 100644 index b594809..0000000 --- a/one-variable-calculus/lake-manifest.json +++ /dev/null @@ -1,28 +0,0 @@ -{"version": 4, - "packagesDir": "lake-packages", - "packages": - [{"path": {"name": "Bookshelf", "dir": "./../shared"}}, - {"git": - {"url": "https://github.com/leanprover-community/mathlib4.git", - "subDir?": null, - "rev": "0107c50abf149a48b5b9ad08a0b2a2093bcb567a", - "name": "mathlib", - "inputRev?": "0107c50abf149a48b5b9ad08a0b2a2093bcb567a"}}, - {"git": - {"url": "https://github.com/gebner/quote4", - "subDir?": null, - "rev": "7ae096b232087096ff0243a2b70d32720d2621ae", - "name": "Qq", - "inputRev?": "master"}}, - {"git": - {"url": "https://github.com/JLimperg/aesop", - "subDir?": null, - "rev": "071464ac36e339afb7a87640aa1f8121f707a59a", - "name": "aesop", - "inputRev?": "master"}}, - {"git": - {"url": "https://github.com/leanprover/std4", - "subDir?": null, - "rev": "5507f9d8409f93b984ce04eccf4914d534e6fca2", - "name": "std", - "inputRev?": "main"}}]} diff --git a/one-variable-calculus/lakefile.lean b/one-variable-calculus/lakefile.lean deleted file mode 100644 index d87456f..0000000 --- a/one-variable-calculus/lakefile.lean +++ /dev/null @@ -1,12 +0,0 @@ -import Lake -open Lake DSL - -package «one-variable-calculus» - -require Bookshelf from "../shared" -require mathlib from git - "https://github.com/leanprover-community/mathlib4.git" @ - "0107c50abf149a48b5b9ad08a0b2a2093bcb567a" - -@[default_target] -lean_lib «apostol» diff --git a/one-variable-calculus/lean-toolchain b/one-variable-calculus/lean-toolchain deleted file mode 100644 index d30699b..0000000 --- a/one-variable-calculus/lean-toolchain +++ /dev/null @@ -1 +0,0 @@ -leanprover/lean4:nightly-2023-04-02 diff --git a/shared/preamble.tex b/preamble.tex similarity index 100% rename from shared/preamble.tex rename to preamble.tex diff --git a/shared/lakefile.lean b/shared/lakefile.lean deleted file mode 100644 index da702ea..0000000 --- a/shared/lakefile.lean +++ /dev/null @@ -1,11 +0,0 @@ -import Lake -open Lake DSL - -package «Bookshelf» - -require mathlib from git - "https://github.com/leanprover-community/mathlib4.git" @ - "0107c50abf149a48b5b9ad08a0b2a2093bcb567a" - -@[default_target] -lean_lib «Bookshelf» diff --git a/shared/lean-toolchain b/shared/lean-toolchain deleted file mode 100644 index d30699b..0000000 --- a/shared/lean-toolchain +++ /dev/null @@ -1 +0,0 @@ -leanprover/lean4:nightly-2023-04-02 diff --git a/theorem-proving-in-lean/Avigad.lean b/theorem-proving-in-lean/Avigad.lean deleted file mode 100644 index 478fb85..0000000 --- a/theorem-proving-in-lean/Avigad.lean +++ /dev/null @@ -1,6 +0,0 @@ -import Avigad.Chapter2 -import Avigad.Chapter3 -import Avigad.Chapter4 -import Avigad.Chapter5 -import Avigad.Chapter7 -import Avigad.Chapter8 diff --git a/theorem-proving-in-lean/lake-manifest.json b/theorem-proving-in-lean/lake-manifest.json deleted file mode 100644 index 1e31dae..0000000 --- a/theorem-proving-in-lean/lake-manifest.json +++ /dev/null @@ -1 +0,0 @@ -{"version": 4, "packagesDir": "lake-packages", "packages": []} diff --git a/theorem-proving-in-lean/lakefile.lean b/theorem-proving-in-lean/lakefile.lean deleted file mode 100644 index a5dd762..0000000 --- a/theorem-proving-in-lean/lakefile.lean +++ /dev/null @@ -1,7 +0,0 @@ -import Lake -open Lake DSL - -package «theorem-proving-in-lean» - -@[default_target] -lean_lib «avigad» diff --git a/theorem-proving-in-lean/lean-toolchain b/theorem-proving-in-lean/lean-toolchain deleted file mode 100644 index d30699b..0000000 --- a/theorem-proving-in-lean/lean-toolchain +++ /dev/null @@ -1 +0,0 @@ -leanprover/lean4:nightly-2023-04-02