symgeoalg

commit 6cd1e492c505b19678418a0938f1bf5c89a42ee8
parent 0460c609533b6724301073f55536c2f8d90d5962
Author: Robert Russell <robertrussell.72001@gmail.com>
Date:   Mon, 22 Jul 2024 23:56:45 -0700

Delete junk from lake init

Diffstat:
M
Main.lean
 | 
4
+---
D
README.md
 | 
2
--
D
Vslean.lean
 | 
4
----
D
Vslean/Basic.lean
 | 
2
--
M
lakefile.lean
 | 
4
----

5 files changed, 1 insertion(+), 15 deletions(-)
diff --git a/Main.lean b/Main.lean
@@ -1,4 +1,2 @@
-import «Vslean»
-
 def main : IO Unit :=
-  IO.println s!"Hello, {hello}!"
+  IO.println "whoa"
diff --git a/README.md b/README.md
@@ -1 +0,0 @@
-# vslean
-\ No newline at end of file
diff --git a/Vslean.lean b/Vslean.lean
@@ -1,3 +0,0 @@
--- 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
@@ -1 +0,0 @@
-def hello := "world"
-\ No newline at end of file
diff --git a/lakefile.lean b/lakefile.lean
@@ -2,10 +2,6 @@ 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