Changes
5 changed files (+114/-0)
-
.gitignore (new)
-
@@ -0,0 +1,1 @@/.lake
-
-
Main.lean (new)
-
@@ -0,0 +1,2 @@import Mathlib def main := IO.println "Hello, world!"
-
-
lake-manifest.json (new)
-
@@ -0,0 +1,95 @@{"version": "1.1.0", "packagesDir": ".lake/packages", "packages": [{"url": "https://github.com/leanprover-community/mathlib4", "type": "git", "subDir": null, "scope": "leanprover-community", "rev": "766e19e781a0992344fd4f24d2662858b6b87250", "name": "mathlib", "manifestFile": "lake-manifest.json", "inputRev": "v4.25.0-rc2", "inherited": false, "configFile": "lakefile.lean"}, {"url": "https://github.com/leanprover-community/plausible", "type": "git", "subDir": null, "scope": "leanprover-community", "rev": "8864a73bf79aad549e34eff972c606343935106d", "name": "plausible", "manifestFile": "lake-manifest.json", "inputRev": "main", "inherited": true, "configFile": "lakefile.toml"}, {"url": "https://github.com/leanprover-community/LeanSearchClient", "type": "git", "subDir": null, "scope": "leanprover-community", "rev": "2ed4ba69b6127de8f5c2af83cccacd3c988b06bf", "name": "LeanSearchClient", "manifestFile": "lake-manifest.json", "inputRev": "main", "inherited": true, "configFile": "lakefile.toml"}, {"url": "https://github.com/leanprover-community/import-graph", "type": "git", "subDir": null, "scope": "leanprover-community", "rev": "451499ea6e97cee4c8979b507a9af5581a849161", "name": "importGraph", "manifestFile": "lake-manifest.json", "inputRev": "main", "inherited": true, "configFile": "lakefile.toml"}, {"url": "https://github.com/leanprover-community/ProofWidgets4", "type": "git", "subDir": null, "scope": "leanprover-community", "rev": "fb8ed0a85a96e3176f6e94b20d413ea72d92576d", "name": "proofwidgets", "manifestFile": "lake-manifest.json", "inputRev": "v0.0.77", "inherited": true, "configFile": "lakefile.lean"}, {"url": "https://github.com/leanprover-community/aesop", "type": "git", "subDir": null, "scope": "leanprover-community", "rev": "1fa48c6a63b4c4cda28be61e1037192776e77ac0", "name": "aesop", "manifestFile": "lake-manifest.json", "inputRev": "master", "inherited": true, "configFile": "lakefile.toml"}, {"url": "https://github.com/leanprover-community/quote4", "type": "git", "subDir": null, "scope": "leanprover-community", "rev": "95c2f8afe09d9e49d3cacca667261da04f7f93f7", "name": "Qq", "manifestFile": "lake-manifest.json", "inputRev": "master", "inherited": true, "configFile": "lakefile.toml"}, {"url": "https://github.com/leanprover-community/batteries", "type": "git", "subDir": null, "scope": "leanprover-community", "rev": "c44068fa1b40041e6df42bd67639b690eb2764ca", "name": "batteries", "manifestFile": "lake-manifest.json", "inputRev": "main", "inherited": true, "configFile": "lakefile.toml"}, {"url": "https://github.com/leanprover/lean4-cli", "type": "git", "subDir": null, "scope": "leanprover", "rev": "72ae7004d9f0ddb422aec5378204fdd7828c5672", "name": "Cli", "manifestFile": "lake-manifest.json", "inputRev": "v4.25.0-rc2", "inherited": true, "configFile": "lakefile.toml"}], "name": "leantest", "lakeDir": ".lake"}
-
-
lakefile.toml (new)
-
@@ -0,0 +1,15 @@name = "leantest" version = "0.1.0" defaultTargets = ["leantest"] [[lean_lib]] name = "Leantest" [[lean_exe]] name = "leantest" root = "Main" [[require]] name = "mathlib" scope = "leanprover-community" rev = "v4.25.0-rc2"
-
-
lean-toolchain (new)
-
@@ -0,0 +1,1 @@leanprover/lean4:v4.25.0-rc2
-