Add basic Lean4 infrastructure and Float package

.gitignore

@@ -1,6 +1,7 @@
 bazel-*
 /.eclipse-bin/
 /.project
+/.lake
 .vscode/
 ryu/*.[oa]
 ryu/tests/*.test

lake-manifest.json

@@ -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": "32d24245c7a12ded17325299fd41d412022cd3fe",
+   "name": "mathlib",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "v4.27.0-rc1",
+   "inherited": false,
+   "configFile": "lakefile.lean"},
+  {"url": "https://github.com/leanprover-community/plausible",
+   "type": "git",
+   "subDir": null,
+   "scope": "leanprover-community",
+   "rev": "8d3713f36dda48467eb61f8c1c4db89c49a6251a",
+   "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": "19e5f5cc9c21199be466ef99489e3acab370f079",
+   "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": "4eb26e1a4806b200ddfe5179d0c2a0fae56c54a7",
+   "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": "ef8377f31b5535430b6753a974d685b0019d0681",
+   "name": "proofwidgets",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "v0.0.84",
+   "inherited": true,
+   "configFile": "lakefile.lean"},
+  {"url": "https://github.com/leanprover-community/aesop",
+   "type": "git",
+   "subDir": null,
+   "scope": "leanprover-community",
+   "rev": "fb12f5535c80e40119286d9575c9393562252d21",
+   "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": "523ec6fc8062d2f470fdc8de6f822fe89552b5e6",
+   "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": "6254bed25866358ce4f841fa5a13b77de04ffbc8",
+   "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": "726b98c53e2da249c1de768fbbbb5e67bc9cef60",
+   "name": "Cli",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "v4.27.0-rc1",
+   "inherited": true,
+   "configFile": "lakefile.toml"}],
+ "name": "ryu",
+ "lakeDir": ".lake"}

lakefile.toml

@@ -0,0 +1,19 @@
+name = "ryu"
+version = "0.1.0"
+keywords = ["math"]
+defaultTargets = ["Ryu"]
+
+[leanOptions]
+pp.unicode.fun = true # pretty-prints `fun a ↦ b`
+relaxedAutoImplicit = false
+weak.linter.mathlibStandardSet = true
+maxSynthPendingDepth = 3
+
+[[require]]
+name = "mathlib"
+scope = "leanprover-community"
+rev = "v4.27.0-rc1"
+
+[[lean_lib]]
+name = "Ryu"
+srcDir = "lean"

lean-toolchain

@@ -0,0 +1 @@
+leanprover/lean4:v4.27.0-rc1

lean/Ryu/Basic.lean

@@ -0,0 +1,7 @@
+import Mathlib
+
+namespace Ryu
+
+-- TODO: Write me.
+
+end Ryu