search

ImperialCollegeLondon / natural_number_game

Building the natural numbers in Lean 3. The original natural number game, now frozen. See README for Lean 4 information.
Apache License 2.0
288 stars 72 forks source link

Drop down menu for levels #87

Closed pglutz closed 4 years ago

pglutz commented 4 years ago

I think it would be helpful to have a drop down menu showing all the levels in the current world. Currently it is a bit annoying to not know how long each world might take. Also it's satisfying to see your progress in a single world accumulate.

kbuzzard commented 4 years ago

This is an issue for the Lean game maker, not the natural number game: https://github.com/mpedramfar/Lean-game-maker

kbuzzard commented 4 years ago

Mohammad did add the "counter" at the top though, so maybe this solves it?