symgeoalg

commit 0460c609533b6724301073f55536c2f8d90d5962
Author: Lean 4 VS Code Extension <>
Date:   Mon, 22 Jul 2024 23:51:23 -0700

Initial commit

Diffstat:
A
.gitignore
 | 
1
+
A
Main.lean
 | 
4
++++
A
README.md
 | 
2
++
A
Vslean.lean
 | 
4
++++
A
Vslean/Basic.lean
 | 
2
++
A
lake-manifest.json
 | 
5
+++++
A
lakefile.lean
 | 
12
++++++++++++
A
lean-toolchain
 | 
1
+

8 files changed, 31 insertions(+), 0 deletions(-)
diff --git a/.gitignore b/.gitignore
@@ -0,0 +1 @@
+/.lake
diff --git a/Main.lean b/Main.lean
@@ -0,0 +1,4 @@
+import «Vslean»
+
+def main : IO Unit :=
+  IO.println s!"Hello, {hello}!"
diff --git a/README.md b/README.md
@@ -0,0 +1 @@
+# vslean
+\ No newline at end of file
diff --git a/Vslean.lean b/Vslean.lean
@@ -0,0 +1,3 @@
+-- This module serves as the root of the `Vslean` library.
+-- Import modules here that should be built as part of the library.
+import «Vslean».Basic
+\ No newline at end of file
diff --git a/Vslean/Basic.lean b/Vslean/Basic.lean
@@ -0,0 +1 @@
+def hello := "world"
+\ No newline at end of file
diff --git a/lake-manifest.json b/lake-manifest.json
@@ -0,0 +1,5 @@
+{"version": "1.0.0",
+ "packagesDir": ".lake/packages",
+ "packages": [],
+ "name": "vslean",
+ "lakeDir": ".lake"}
diff --git a/lakefile.lean b/lakefile.lean
@@ -0,0 +1,12 @@
+import Lake
+open Lake DSL
+
+package «vslean» where
+  -- add package configuration options here
+
+lean_lib «Vslean» where
+  -- add library configuration options here
+
+@[default_target]
+lean_exe «vslean» where
+  root := `Main
diff --git a/lean-toolchain b/lean-toolchain
@@ -0,0 +1 @@
+leanprover/lean4:stable