Initial commit

.gitignore

@@ -0,0 +1 @@
+/.lake

LeanGraphics.lean

@@ -0,0 +1,3 @@
+-- This module serves as the root of the `LeanGraphics` library.
+-- Import modules here that should be built as part of the library.
+import LeanGraphics.Basic

LeanGraphics/Basic.lean

@@ -0,0 +1 @@
+def startupMsg := "Lean4 graphics test"

Main.lean

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

README.md

@@ -0,0 +1,9 @@
+# lean-graphics
+
+
+This is an experiment in writing GUI programs using Lean4.
+
+## Prior art
+
+- Lean4 SDL3 bindings: https://github.com/ValorZard/lean-sdl3 and https://github.com/ValorZard/lean-sdl-test
+- Doom-like game: https://github.com/oOo0oOo/LeanDoomed

justfile

@@ -0,0 +1,7 @@
+_default:
+    @just --list
+
+
+# Run main binary
+run:
+    lake exec lean-graphics

lake-manifest.json

@@ -0,0 +1,5 @@
+{"version": "1.1.0",
+ "packagesDir": ".lake/packages",
+ "packages": [],
+ "name": "«lean-graphics»",
+ "lakeDir": ".lake"}

lakefile.toml

@@ -0,0 +1,10 @@
+name = "lean-graphics"
+version = "0.1.0"
+defaultTargets = ["lean-graphics"]
+
+[[lean_lib]]
+name = "LeanGraphics"
+
+[[lean_exe]]
+name = "lean-graphics"
+root = "Main"

lean-toolchain

@@ -0,0 +1 @@
+leanprover/lean4:v4.25.2