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.

The games built with this library work best in Chrome and Firefox.

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.