From 5382d1572b40c50fb9181d3c22fce7b48e8c7542 Mon Sep 17 00:00:00 2001
From: Stefan Kebekus <kebekus@users.noreply.github.com>
Date: Tue, 23 Apr 2024 09:18:45 +0200
Subject: [PATCH] Add files

---
 .gitignore           |  2 ++
 Nevanlinna.lean      |  1 +
 lake-manifest.json   | 68 ++++++++++++++++++++++++++++++++++++++++++++
 lakefile.lean        | 14 +++++++++
 lean-toolchain       |  1 +
 nevanlinna/test.lean |  1 +
 6 files changed, 87 insertions(+)
 create mode 100644 .gitignore
 create mode 100644 Nevanlinna.lean
 create mode 100644 lake-manifest.json
 create mode 100644 lakefile.lean
 create mode 100644 lean-toolchain
 create mode 100644 nevanlinna/test.lean

diff --git a/.gitignore b/.gitignore
new file mode 100644
index 0000000..20c60d7
--- /dev/null
+++ b/.gitignore
@@ -0,0 +1,2 @@
+/build
+/lake-packages/*
diff --git a/Nevanlinna.lean b/Nevanlinna.lean
new file mode 100644
index 0000000..e99d3a6
--- /dev/null
+++ b/Nevanlinna.lean
@@ -0,0 +1 @@
+def hello := "world"
\ No newline at end of file
diff --git a/lake-manifest.json b/lake-manifest.json
new file mode 100644
index 0000000..67d262b
--- /dev/null
+++ b/lake-manifest.json
@@ -0,0 +1,68 @@
+{"version": 7,
+ "packagesDir": ".lake/packages",
+ "packages":
+ [{"url": "https://github.com/leanprover/std4",
+   "type": "git",
+   "subDir": null,
+   "rev": "e840c18f7334c751efbd4cfe531476e10c943cdb",
+   "name": "std",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "main",
+   "inherited": true,
+   "configFile": "lakefile.lean"},
+  {"url": "https://github.com/leanprover-community/quote4",
+   "type": "git",
+   "subDir": null,
+   "rev": "64365c656d5e1bffa127d2a1795f471529ee0178",
+   "name": "Qq",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "master",
+   "inherited": true,
+   "configFile": "lakefile.lean"},
+  {"url": "https://github.com/leanprover-community/aesop",
+   "type": "git",
+   "subDir": null,
+   "rev": "5fefb40a7c9038a7150e7edd92e43b1b94c49e79",
+   "name": "aesop",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "master",
+   "inherited": true,
+   "configFile": "lakefile.lean"},
+  {"url": "https://github.com/leanprover-community/ProofWidgets4",
+   "type": "git",
+   "subDir": null,
+   "rev": "fb65c476595a453a9b8ffc4a1cea2db3a89b9cd8",
+   "name": "proofwidgets",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "v0.0.30",
+   "inherited": true,
+   "configFile": "lakefile.lean"},
+  {"url": "https://github.com/leanprover/lean4-cli",
+   "type": "git",
+   "subDir": null,
+   "rev": "be8fa79a28b8b6897dce0713ef50e89c4a0f6ef5",
+   "name": "Cli",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "main",
+   "inherited": true,
+   "configFile": "lakefile.lean"},
+  {"url": "https://github.com/leanprover-community/import-graph.git",
+   "type": "git",
+   "subDir": null,
+   "rev": "61a79185b6582573d23bf7e17f2137cd49e7e662",
+   "name": "importGraph",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "main",
+   "inherited": true,
+   "configFile": "lakefile.lean"},
+  {"url": "https://github.com/leanprover-community/mathlib4.git",
+   "type": "git",
+   "subDir": null,
+   "rev": "e408da18380ef42acf7b8337c6b0536bfac09105",
+   "name": "mathlib",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": null,
+   "inherited": false,
+   "configFile": "lakefile.lean"}],
+ "name": "nevanlinna",
+ "lakeDir": ".lake"}
diff --git a/lakefile.lean b/lakefile.lean
new file mode 100644
index 0000000..ab1bdc9
--- /dev/null
+++ b/lakefile.lean
@@ -0,0 +1,14 @@
+import Lake
+open Lake DSL
+
+package «nevanlinna» {
+  -- add any package configuration options here
+}
+
+require mathlib from git
+  "https://github.com/leanprover-community/mathlib4.git"
+
+@[default_target]
+lean_lib «Nevanlinna» {
+  -- add any library configuration options here
+}
diff --git a/lean-toolchain b/lean-toolchain
new file mode 100644
index 0000000..9ad3040
--- /dev/null
+++ b/lean-toolchain
@@ -0,0 +1 @@
+leanprover/lean4:v4.7.0
diff --git a/nevanlinna/test.lean b/nevanlinna/test.lean
new file mode 100644
index 0000000..8b13789
--- /dev/null
+++ b/nevanlinna/test.lean
@@ -0,0 +1 @@
+