From f056628881ecf26fb446377d8666cad8eba970cd Mon Sep 17 00:00:00 2001
From: mehbark <terezi@pyrope.net>
Date: Thu, 18 Sep 2025 14:17:02 -0400
Subject: [PATCH] initial go

---
 .github/workflows/lean_action_ci.yml | 14 +++++++++++++
 .gitignore                           |  1 +
 Main.lean                            | 30 ++++++++++++++++++++++++++++
 README.md                            |  1 +
 lake-manifest.json                   |  5 +++++
 lakefile.toml                        |  7 +++++++
 lean-toolchain                       |  1 +
 7 files changed, 59 insertions(+)
 create mode 100644 .github/workflows/lean_action_ci.yml
 create mode 100644 .gitignore
 create mode 100644 Main.lean
 create mode 100644 README.md
 create mode 100644 lake-manifest.json
 create mode 100644 lakefile.toml
 create mode 100644 lean-toolchain

diff --git a/.github/workflows/lean_action_ci.yml b/.github/workflows/lean_action_ci.yml
new file mode 100644
index 0000000..09cd4ca
--- /dev/null
+++ b/.github/workflows/lean_action_ci.yml
@@ -0,0 +1,14 @@
+name: Lean Action CI
+
+on:
+  push:
+  pull_request:
+  workflow_dispatch:
+
+jobs:
+  build:
+    runs-on: ubuntu-latest
+
+    steps:
+      - uses: actions/checkout@v4
+      - uses: leanprover/lean-action@v1
diff --git a/.gitignore b/.gitignore
new file mode 100644
index 0000000..bfb30ec
--- /dev/null
+++ b/.gitignore
@@ -0,0 +1 @@
+/.lake
diff --git a/Main.lean b/Main.lean
new file mode 100644
index 0000000..5d18778
--- /dev/null
+++ b/Main.lean
@@ -0,0 +1,30 @@
+inductive Op : (inp out : Array (Type u)) → Type (u+1) where
+| push (a : α)        : Op #[] #[α]
+| pop  {α : Type u}   : Op #[α] #[]
+| dup  {α : Type u}   : Op #[α] #[α, α]
+| swap {α β : Type u} : Op #[α, β] #[β, α]
+| call (f : α → β)    : Op #[α] #[β]
+| seq  (a : Op i o) (b : Op o o') : Op i o'
+
+instance : HAndThen (Op i o) (Op o o') (Op i o') where
+  hAndThen a b := Op.seq a (b ())
+
+abbrev Stack : Array Type → Type
+| ⟨[]⟩ => Unit
+| ⟨[t]⟩ => t
+| ⟨t::ts⟩ => t × Stack ⟨ts⟩
+
+#reduce (types := true) Stack #[Nat, Int, Int]
+
+def Op.run : Op i o → Stack i → Stack o
+| push x, () => x
+| pop, _ => ()
+| dup, x => (x, x)
+| swap, (a, b) => (b, a)
+| call f, x => f x
+| seq a b, s => b.run (a.run s)
+
+#eval Op.push 1 >> Op.call Nat.succ |>.run ()
+
+def main : IO Unit :=
+  IO.println s!"Hello, world!"
diff --git a/README.md b/README.md
new file mode 100644
index 0000000..4bac601
--- /dev/null
+++ b/README.md
@@ -0,0 +1 @@
+# puyo
\ No newline at end of file
diff --git a/lake-manifest.json b/lake-manifest.json
new file mode 100644
index 0000000..e459772
--- /dev/null
+++ b/lake-manifest.json
@@ -0,0 +1,5 @@
+{"version": "1.1.0",
+ "packagesDir": ".lake/packages",
+ "packages": [],
+ "name": "puyo",
+ "lakeDir": ".lake"}
diff --git a/lakefile.toml b/lakefile.toml
new file mode 100644
index 0000000..4d07dd8
--- /dev/null
+++ b/lakefile.toml
@@ -0,0 +1,7 @@
+name = "puyo"
+version = "0.1.0"
+defaultTargets = ["puyo"]
+
+[[lean_exe]]
+name = "puyo"
+root = "Main"
diff --git a/lean-toolchain b/lean-toolchain
new file mode 100644
index 0000000..7f254a9
--- /dev/null
+++ b/lean-toolchain
@@ -0,0 +1 @@
+leanprover/lean4:v4.23.0