leanprover-community / lean4game

Server to host lean games.
https://adam.math.hhu.de
GNU General Public License v3.0
199 stars 35 forks source link

More consistent naming of “difficulty: playground / explorer / regular” #97

Closed TentativeConvert closed 1 year ago

TentativeConvert commented 1 year ago

Some ideas:

In any case, it should be made clear what the default setting is.

abentkamp commented 1 year ago

I love "Game rules: none / lax / regular". Seems very self-explanatory.

joneugster commented 1 year ago

sounds good to me.