Update create_game.md
This commit is contained in:
@@ -243,6 +243,10 @@ Hint "now use `rw [{h}]` to use your assumption {h}."
|
||||
```
|
||||
That way, the game will replace it with the actual name the assumption has in the player's proof state.
|
||||
|
||||
## 7. Update your game
|
||||
|
||||
In principle, it is as simple as modifying `lean-toolchain` to update your game to a new Lean version. However, you should read about the details in [Update An Existing Game](https://github.com/leanprover-community/lean4game/edit/main/doc/update_game.md).
|
||||
|
||||
## Further Notes
|
||||
|
||||
Here are some random further things you should consider designing a new game:
|
||||
|
||||
Reference in New Issue
Block a user