From 9bba78eb1d4a1597675c441af2e008a2cb0dbb7e Mon Sep 17 00:00:00 2001 From: Leni Aniva Date: Sun, 7 May 2023 15:19:45 -0700 Subject: [PATCH] Initial commit --- .gitignore | 2 ++ Main.lean | 4 ++++ Pantograph.lean | 1 + lakefile.lean | 19 +++++++++++++++++++ lean-toolchain | 1 + 5 files changed, 27 insertions(+) create mode 100644 .gitignore create mode 100644 Main.lean create mode 100644 Pantograph.lean create mode 100644 lakefile.lean create mode 100644 lean-toolchain 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