leanprover-community
Don't show locked items in inventory.
When you start playing a game that eventually unlocks a lot of theorems/definitions/tactics, you see them in the inventory from the beginning (in a different color and with a lock sign, but they are visible). This can be overwhelming for the people that play the game from the beginning.
I propose to only show the items that are unlocked. This would also have the advantage of making the progress in the game more rewarding for the player, since (s)he would see the inventory grow as (s)he progresses in the game.
I liked it showing the locked items. Gives you an idea of the scope of the game & how much progress you've made.
Showing the locked items has been an active design decision which has been made in order to give the player some curiosity about what's still to come. I think that's not going to change.
However, I'm now trying to create a version 2 of the game server and I'll keep this in mind. Maybe an option to hide them would be appropriate?
