leanprover-community/lean4game

feat: add bonus levels

joneugster opened this issue · 0 comments

Add an option that worlds can be marked as completed before finishing all levels.

  • In the level files (.lean) add a command FinalLevel which when added after Level xy marks the last compulory level.
  • Mark bonus levels pastel golden (?) in the world overview (or a bit darker golden if playable)
  • Once the final level is completed:
    • unlock the next worlds
    • always display two buttons "Leave world" and "Bonus" (or the existing "Next") as long as there are still bonus levels.