fracting/Lean-game-maker

This project converts structured Lean code into an interactive browser game.

Lean Game Maker

This library renders structured Lean files into an interactive game with a javascript Lean server running on the browser. See the Natural number game for an implementation of this game.

Installation

See the installation guide.

Usage

See the usage guide.

Acknowledgements

Special thanks to Bryan Gin-ge Chen and Patrick Massot. This project uses some codes from Bryan's fork of the lean-web-editor and Patrick's Lean formatter.