search

leanprover-community / lean4game

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

NNG talks about Hypotheses, UI has Assumptions #271

Open jackie-scholl opened 1 month ago

jackie-scholl commented 1 month ago

I loved playing the Natural Number Game, but I found it very confusing when the sidebar text talked about "hypotheses" - I think these are the same as the "assumptions" listed in the game window, although even now I'm not 100% sure. I think if they are different it would be helpful to explain what a hypothesis is at first use, and if they're the same it would be helpful to use the same term consistently.

joneugster commented 1 month ago

They are the same, and the UI's distinction between "Objects" and "Assumptions" is also merely an arificial one. (i.e. it lists anything who's type is of type Prop as "assumption" and everything else as "object")

Sounds reasonable to adjust the wording in the NNG!