PuzzleScript reimplementation in Lean, heavily vibe-coded (except Engine and its dependencies, State on JS side, showcase files)
- Lean 48.4%
- JavaScript 26.5%
- Python 25.1%
| demos | ||
| js | ||
| PuzzleScript | ||
| tools | ||
| Bench.lean | ||
| CLAUDE.md | ||
| DEBUGGING.md | ||
| Demo.lean | ||
| DemoGames.lean | ||
| engine_pseudocode_js.py | ||
| ExportBoardState.lean | ||
| ExportRules.lean | ||
| lakefile.toml | ||
| lean-toolchain | ||
| PuzzleScript.lean | ||
| README.md | ||
| rule_match_pseudocode.py | ||
PuzzleScript in Lean
This is a Lean implementation of the PuzzleScript game engine.
Features:
- Loading games in PuzzleScript format into Lean expression.
- Playing games in Lean's infoview
- Checking solvability by loading exported solutions
Start files:
- I just want to play games: DemoGames.lean
- I want to understand the basics of this Lean implementation: Demo.lean