diff --git a/one-variable-calculus/Apostol.lean b/one-variable-calculus/Apostol.lean new file mode 100644 index 0000000..e99d3a6 --- /dev/null +++ b/one-variable-calculus/Apostol.lean @@ -0,0 +1 @@ +def hello := "world" \ No newline at end of file diff --git a/one-variable-calculus/lake-manifest.json b/one-variable-calculus/lake-manifest.json new file mode 100644 index 0000000..59662d6 --- /dev/null +++ b/one-variable-calculus/lake-manifest.json @@ -0,0 +1,28 @@ +{"version": 4, + "packagesDir": "lake-packages", + "packages": + [{"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"}}, + {"path": {"name": "Common", "dir": "./../common"}}]} diff --git a/one-variable-calculus/lakefile.lean b/one-variable-calculus/lakefile.lean new file mode 100644 index 0000000..a2e6da4 --- /dev/null +++ b/one-variable-calculus/lakefile.lean @@ -0,0 +1,12 @@ +import Lake +open Lake DSL + +package «one-variable-calculus» + +require Common from "../common" +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 new file mode 100644 index 0000000..d30699b --- /dev/null +++ b/one-variable-calculus/lean-toolchain @@ -0,0 +1 @@ +leanprover/lean4:nightly-2023-04-02