Use consistent naming scheme, update depsHEADmaster

12 files changed, 27 insertions, 22 deletions

diff --git a/ac.lean b/Choice.lean
index 7a7522c..7a7522c 100644
--- a/ac.lean
+++ b/Choice.lean
diff --git a/gcd.lean b/Gcd.lean
index fa9bf7b..cead114 100644
--- a/gcd.lean
+++ b/Gcd.lean
@@ -5,10 +5,14 @@ decreasing_by
   rename_i h
   exact Nat.mod_lt a h
 
-#eval "test"
-
 def N := 1000
 
 def A := List.range N
 
-#eval (A.map λ x => (A.map λ y => gcd x y).sum).sum
+def sum := (A.map λ x => (A.map λ y => gcd x y).sum).sum
+
+#eval sum
+
+def main := do
+  IO.println "test"
+  IO.println sum
diff --git a/lambcalc.lean b/LambCalc.lean
index 1993696..1993696 100644
--- a/lambcalc.lean
+++ b/LambCalc.lean
diff --git a/lazy.lean b/Lazy.lean
index 319e2f2..319e2f2 100644
--- a/lazy.lean
+++ b/Lazy.lean
diff --git a/monad.lean b/Monad.lean
index 7ece1d6..7ece1d6 100644
--- a/monad.lean
+++ b/Monad.lean
diff --git a/native-decide.lean b/NativeDecide.lean
index ac0c0ac..ac0c0ac 100644
--- a/native-decide.lean
+++ b/NativeDecide.lean
diff --git a/palin.lean b/Palin.lean
index f8efa9f..f8efa9f 100644
--- a/palin.lean
+++ b/Palin.lean
diff --git a/sum.lean b/Sum.lean
index 9ceeb0a..9ceeb0a 100644
--- a/sum.lean
+++ b/Sum.lean
diff --git a/typedlambcalc.lean b/TypedLambCalc.lean
index d4b445d..d4b445d 100644
--- a/typedlambcalc.lean
+++ b/TypedLambCalc.lean
diff --git a/lake-manifest.json b/lake-manifest.json
index dc28e87..f5e6387 100644
--- a/lake-manifest.json
+++ b/lake-manifest.json
@@ -5,7 +5,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "826aa6f3fab98e8a5dd34dbe2f901127b603039e",
+   "rev": "84a77eea345d5b6f36803f8780c09d52c876d51f",
    "name": "mathlib",
    "manifestFile": "lake-manifest.json",
    "inputRev": "master",
@@ -15,17 +15,17 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "304c5e2f490d546134c06bf8919e13b175272084",
+   "rev": "fde3fc21dd68a10791dea22b6f5b53c5a5a5962d",
    "name": "plausible",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "main",
+   "inputRev": "nightly-testing",
    "inherited": true,
    "configFile": "lakefile.toml"},
   {"url": "https://github.com/leanprover-community/LeanSearchClient",
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "25078369972d295301f5a1e53c3e5850cf6d9d4c",
+   "rev": "6c62474116f525d2814f0157bb468bf3a4f9f120",
    "name": "LeanSearchClient",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -35,57 +35,57 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "f5e58ef1f58fc0cbd92296d18951f45216309e48",
+   "rev": "856a8cb8908af109aac3ce13e2b4f866f3d75199",
    "name": "importGraph",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "main",
+   "inputRev": "nightly-testing",
    "inherited": true,
    "configFile": "lakefile.toml"},
   {"url": "https://github.com/leanprover-community/ProofWidgets4",
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "632ca63a94f47dbd5694cac3fd991354b82b8f7a",
+   "rev": "2d6d124aedc3023506a67e50bfd5582384d6bd17",
    "name": "proofwidgets",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "v0.0.59",
+   "inputRev": "v0.0.63-pre",
    "inherited": true,
    "configFile": "lakefile.lean"},
   {"url": "https://github.com/leanprover-community/aesop",
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "417f5fba2ea46d1117c5a8d795d383062b02688e",
+   "rev": "a1b5d59f433c6ec2b318192bd910c257a3c62be8",
    "name": "aesop",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "master",
+   "inputRev": "nightly-testing",
    "inherited": true,
    "configFile": "lakefile.toml"},
   {"url": "https://github.com/leanprover-community/quote4",
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "36ce5e17d6ab3c881e0cb1bb727982507e708130",
+   "rev": "56047303fce0d07dcae7e3e91b17eef67d11f6f4",
    "name": "Qq",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "master",
+   "inputRev": "nightly-testing",
    "inherited": true,
    "configFile": "lakefile.toml"},
   {"url": "https://github.com/leanprover-community/batteries",
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "1a8afbb6f95c4de139dca63cc7454862cb54099a",
+   "rev": "3613427d66262c4e25e19b40a6a49242e94ba072",
    "name": "batteries",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "main",
+   "inputRev": "nightly-testing",
    "inherited": true,
    "configFile": "lakefile.toml"},
   {"url": "https://github.com/leanprover/lean4-cli",
    "type": "git",
    "subDir": null,
    "scope": "leanprover",
-   "rev": "4f22c09e7ded721e6ecd3cf59221c4647ca49664",
+   "rev": "1604206fcd0462da9a241beeac0e2df471647435",
    "name": "Cli",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
diff --git a/lakefile.toml b/lakefile.toml
index e436535..5b63d6e 100644
--- a/lakefile.toml
+++ b/lakefile.toml
@@ -2,13 +2,14 @@ name = "leantest"
 version = "0.1.0"
 defaultTargets = ["leantest"]
 
-[[lean_lib]]
-name = "Leantest"
-
 [[lean_exe]]
 name = "leantest"
 root = "Main"
 
+[[lean_exe]]
+name = "gcd"
+root = "Gcd"
+
 [[require]]
 name = "mathlib"
 scope = "leanprover-community"
\ No newline at end of file
diff --git a/lean-toolchain b/lean-toolchain
index cc6fba8..bfcebb1 100644
--- a/lean-toolchain
+++ b/lean-toolchain
@@ -1 +1 @@
-leanprover/lean4:v4.20.0-rc5
\ No newline at end of file
+leanprover/lean4:v4.22.0-rc2