commit 9bba78eb1d4a1597675c441af2e008a2cb0dbb7e Author: Leni Aniva Date: Sun May 7 15:19:45 2023 -0700 Initial commit diff --git a/.gitignore b/.gitignore new file mode 100644 index 0000000..2ee099a --- /dev/null +++ b/.gitignore @@ -0,0 +1,2 @@ +/build +/lake-packages diff --git a/Main.lean b/Main.lean new file mode 100644 index 0000000..30cb991 --- /dev/null +++ b/Main.lean @@ -0,0 +1,4 @@ +import Pantograph + +def main : IO Unit := + IO.println s!"Hello, {hello}!" diff --git a/Pantograph.lean b/Pantograph.lean new file mode 100644 index 0000000..e99d3a6 --- /dev/null +++ b/Pantograph.lean @@ -0,0 +1 @@ +def hello := "world" \ No newline at end of file diff --git a/lakefile.lean b/lakefile.lean new file mode 100644 index 0000000..546a324 --- /dev/null +++ b/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 +} diff --git a/lean-toolchain b/lean-toolchain new file mode 100644 index 0000000..a7041bc --- /dev/null +++ b/lean-toolchain @@ -0,0 +1 @@ +leanprover/lean4:nightly-2023-05-06