Initial commit

.gitignore

@@ -0,0 +1,2 @@
+/build
+/lake-packages

Main.lean

@@ -0,0 +1,4 @@
+import Pantograph
+
+def main : IO Unit :=
+  IO.println s!"Hello, {hello}!"

Pantograph.lean

@@ -0,0 +1 @@
+def hello := "world"

lakefile.lean

@@ -0,0 +1,19 @@
+import Lake
+open Lake DSL
+
+
+package pantograph {
+  -- add package configuration options here
+}
+
+require mathlib from git
+  "https://github.com/leanprover-community/mathlib4.git" @  "8e5a00a8afc8913c0584cb85f37951995275fd87"
+
+lean_lib Pantograph {
+  -- add library configuration options here
+}
+
+@[default_target]
+lean_exe pantograph {
+  root := `Main
+}

lean-toolchain

@@ -0,0 +1 @@
+leanprover/lean4:nightly-2023-05-06