From b8d754ea5e409cfe77461320586ab27c56f8af8a Mon Sep 17 00:00:00 2001
From: Joshua Potter <jrpotter2112@gmail.com>
Date: Sun, 9 Apr 2023 12:11:20 -0600
Subject: [PATCH] Add `one-variable-calculus` project.

---
 one-variable-calculus/Apostol.lean       |  1 +
 one-variable-calculus/lake-manifest.json | 28 ++++++++++++++++++++++++
 one-variable-calculus/lakefile.lean      | 12 ++++++++++
 one-variable-calculus/lean-toolchain     |  1 +
 4 files changed, 42 insertions(+)
 create mode 100644 one-variable-calculus/Apostol.lean
 create mode 100644 one-variable-calculus/lake-manifest.json
 create mode 100644 one-variable-calculus/lakefile.lean
 create mode 100644 one-variable-calculus/lean-toolchain

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